YES 4.109
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ IFR
mainModule List
|
| ((union :: Eq a => [[a]] -> [[a]] -> [[a]]) :: Eq a => [[a]] -> [[a]] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | _ _ [] | = | [] |
| deleteBy | eq x (y : ys) | = | if x `eq` y then ys else y : deleteBy eq x ys |
|
| | elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
| elem_by | _ _ [] | = | False |
| elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| | nubBy :: (a -> a -> Bool) -> [a] -> [a]
| nubBy | eq l | = |
| nubBy' l [] | where |
| nubBy' | [] _ | = | [] |
| nubBy' | (y : ys) xs | |
| | | elem_by eq y xs | = |
|
| | | otherwise | = |
|
|
|
|
|
|
| | union :: Eq a => [a] -> [a] -> [a]
|
| | unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
If Reductions:
The following If expression
if eq x y then ys else y : deleteBy eq x ys
is transformed to
| deleteBy0 | ys y eq x True | = ys |
| deleteBy0 | ys y eq x False | = y : deleteBy eq x ys |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule List
|
| ((union :: Eq a => [[a]] -> [[a]] -> [[a]]) :: Eq a => [[a]] -> [[a]] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | _ _ [] | = | [] |
| deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
| |
| deleteBy0 | ys y eq x True | = | ys |
| deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| | elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
| elem_by | _ _ [] | = | False |
| elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| | nubBy :: (a -> a -> Bool) -> [a] -> [a]
| nubBy | eq l | = |
| nubBy' l [] | where |
| nubBy' | [] _ | = | [] |
| nubBy' | (y : ys) xs | |
| | | elem_by eq y xs | = |
|
| | | otherwise | = |
|
|
|
|
|
|
| | union :: Eq a => [a] -> [a] -> [a]
|
| | unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
|
| ((union :: Eq a => [[a]] -> [[a]] -> [[a]]) :: Eq a => [[a]] -> [[a]] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | vw vx [] | = | [] |
| deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
| |
| deleteBy0 | ys y eq x True | = | ys |
| deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| | elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
| elem_by | vz wu [] | = | False |
| elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| | nubBy :: (a -> a -> Bool) -> [a] -> [a]
| nubBy | eq l | = |
| nubBy' l [] | where |
| nubBy' | [] vy | = | [] |
| nubBy' | (y : ys) xs | |
| | | elem_by eq y xs | = |
|
| | | otherwise | = |
|
|
|
|
|
|
| | union :: Eq a => [a] -> [a] -> [a]
|
| | unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Cond Reductions:
The following Function with conditions
| nubBy' | [] vy | = [] |
| nubBy' | (y : ys) xs |
| | | elem_by eq y xs | |
| | | otherwise | |
|
is transformed to
| nubBy' | [] vy | = nubBy'3 [] vy |
| nubBy' | (y : ys) xs | = nubBy'2 (y : ys) xs |
| nubBy'1 | y ys xs True | = nubBy' ys xs |
| nubBy'1 | y ys xs False | = nubBy'0 y ys xs otherwise |
| nubBy'0 | y ys xs True | = y : nubBy' ys (y : xs) |
| nubBy'2 | (y : ys) xs | = nubBy'1 y ys xs (elem_by eq y xs) |
| nubBy'3 | [] vy | = [] |
| nubBy'3 | yx yy | = nubBy'2 yx yy |
The following Function with conditions
is transformed to
| undefined0 | True | = undefined |
| undefined1 | | = undefined0 False |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule List
|
| ((union :: Eq a => [[a]] -> [[a]] -> [[a]]) :: Eq a => [[a]] -> [[a]] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | vw vx [] | = | [] |
| deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
| |
| deleteBy0 | ys y eq x True | = | ys |
| deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| | elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
| elem_by | vz wu [] | = | False |
| elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| | nubBy :: (a -> a -> Bool) -> [a] -> [a]
| nubBy | eq l | = |
| nubBy' l [] | where |
| nubBy' | [] vy | = | nubBy'3 [] vy |
| nubBy' | (y : ys) xs | = | nubBy'2 (y : ys) xs |
|
| nubBy'0 | y ys xs True | = | y : nubBy' ys (y : xs) |
|
| nubBy'1 | y ys xs True | = | nubBy' ys xs |
| nubBy'1 | y ys xs False | = | nubBy'0 y ys xs otherwise |
|
| nubBy'2 | (y : ys) xs | = | nubBy'1 y ys xs (elem_by eq y xs) |
|
| nubBy'3 | [] vy | = | [] |
| nubBy'3 | yx yy | = | nubBy'2 yx yy |
|
|
|
|
| | union :: Eq a => [a] -> [a] -> [a]
|
| | unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Let/Where Reductions:
The bindings of the following Let/Where expression
| nubBy' l [] |
| where |
| nubBy' | [] vy | = nubBy'3 [] vy |
| nubBy' | (y : ys) xs | = nubBy'2 (y : ys) xs |
|
|
| nubBy'0 | y ys xs True | = y : nubBy' ys (y : xs) |
|
|
| nubBy'1 | y ys xs True | = nubBy' ys xs |
| nubBy'1 | y ys xs False | = nubBy'0 y ys xs otherwise |
|
|
| nubBy'2 | (y : ys) xs | = nubBy'1 y ys xs (elem_by eq y xs) |
|
|
| nubBy'3 | [] vy | = [] |
| nubBy'3 | yx yy | = nubBy'2 yx yy |
|
are unpacked to the following functions on top level
| nubByNubBy'3 | yz [] vy | = [] |
| nubByNubBy'3 | yz yx yy | = nubByNubBy'2 yz yx yy |
| nubByNubBy'0 | yz y ys xs True | = y : nubByNubBy' yz ys (y : xs) |
| nubByNubBy'2 | yz (y : ys) xs | = nubByNubBy'1 yz y ys xs (elem_by yz y xs) |
| nubByNubBy'1 | yz y ys xs True | = nubByNubBy' yz ys xs |
| nubByNubBy'1 | yz y ys xs False | = nubByNubBy'0 yz y ys xs otherwise |
| nubByNubBy' | yz [] vy | = nubByNubBy'3 yz [] vy |
| nubByNubBy' | yz (y : ys) xs | = nubByNubBy'2 yz (y : ys) xs |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
mainModule List
|
| (union :: Eq a => [[a]] -> [[a]] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | vw vx [] | = | [] |
| deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
| |
| deleteBy0 | ys y eq x True | = | ys |
| deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| | elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
| elem_by | vz wu [] | = | False |
| elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| | nubBy :: (a -> a -> Bool) -> [a] -> [a]
| nubBy | eq l | = | nubByNubBy' eq l [] |
|
| |
| nubByNubBy' | yz [] vy | = | nubByNubBy'3 yz [] vy |
| nubByNubBy' | yz (y : ys) xs | = | nubByNubBy'2 yz (y : ys) xs |
|
| |
| nubByNubBy'0 | yz y ys xs True | = | y : nubByNubBy' yz ys (y : xs) |
|
| |
| nubByNubBy'1 | yz y ys xs True | = | nubByNubBy' yz ys xs |
| nubByNubBy'1 | yz y ys xs False | = | nubByNubBy'0 yz y ys xs otherwise |
|
| |
| nubByNubBy'2 | yz (y : ys) xs | = | nubByNubBy'1 yz y ys xs (elem_by yz y xs) |
|
| |
| nubByNubBy'3 | yz [] vy | = | [] |
| nubByNubBy'3 | yz yx yy | = | nubByNubBy'2 yz yx yy |
|
| | union :: Eq a => [a] -> [a] -> [a]
|
| | unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(zu7000), Succ(zu36001000)) → new_primPlusNat(zu7000, zu36001000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(zu7000), Succ(zu36001000)) → new_primPlusNat(zu7000, zu36001000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(zu31100100), Succ(zu3600100)) → new_primMulNat(zu31100100, Succ(zu3600100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(zu31100100), Succ(zu3600100)) → new_primMulNat(zu31100100, Succ(zu3600100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(zu3110000), Succ(zu360000)) → new_primEqNat(zu3110000, zu360000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(zu3110000), Succ(zu360000)) → new_primEqNat(zu3110000, zu360000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs3(Right(zu311000), Right(zu36000), gf, app(app(ty_@2, bda), bdb)) → new_esEs2(zu311000, zu36000, bda, bdb)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), app(ty_[], da), cc, cd) → new_esEs1(zu311000, zu36000, da)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, cc, app(app(ty_Either, fh), ga)) → new_esEs3(zu311002, zu36002, fh, ga)
new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), gd, app(app(ty_@2, bag), bah)) → new_esEs2(zu311001, zu36001, bag, bah)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, app(app(ty_@2, ed), ee), cd) → new_esEs2(zu311001, zu36001, ed, ee)
new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), gd, app(ty_Maybe, bab)) → new_esEs(zu311001, zu36001, bab)
new_esEs(Just(zu311000), Just(zu36000), app(app(app(ty_@3, bb), bc), bd)) → new_esEs0(zu311000, zu36000, bb, bc, bd)
new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), app(ty_Maybe, ha), ge) → new_esEs(zu311000, zu36000, ha)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, app(ty_[], ec), cd) → new_esEs1(zu311001, zu36001, ec)
new_esEs3(Right(zu311000), Right(zu36000), gf, app(app(ty_Either, bdc), bdd)) → new_esEs3(zu311000, zu36000, bdc, bdd)
new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), gh) → new_esEs1(zu311011, zu36011, gh)
new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), app(app(ty_@2, hf), hg), ge) → new_esEs2(zu311000, zu36000, hf, hg)
new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), app(ty_[], gc)) → new_esEs1(zu311010, zu36010, gc)
new_esEs(Just(zu311000), Just(zu36000), app(ty_Maybe, ba)) → new_esEs(zu311000, zu36000, ba)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, app(app(app(ty_@3, dh), ea), eb), cd) → new_esEs0(zu311001, zu36001, dh, ea, eb)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), app(app(ty_@2, db), dc), cc, cd) → new_esEs2(zu311000, zu36000, db, dc)
new_esEs3(Right(zu311000), Right(zu36000), gf, app(app(app(ty_@3, bce), bcf), bcg)) → new_esEs0(zu311000, zu36000, bce, bcf, bcg)
new_esEs3(Left(zu311000), Left(zu36000), app(app(ty_Either, bcb), bcc), gg) → new_esEs3(zu311000, zu36000, bcb, bcc)
new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), app(ty_[], he), ge) → new_esEs1(zu311000, zu36000, he)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, cc, app(ty_[], fd)) → new_esEs1(zu311002, zu36002, fd)
new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), app(app(ty_Either, gf), gg)) → new_esEs3(zu311010, zu36010, gf, gg)
new_esEs3(Left(zu311000), Left(zu36000), app(app(app(ty_@3, bbd), bbe), bbf), gg) → new_esEs0(zu311000, zu36000, bbd, bbe, bbf)
new_esEs(Just(zu311000), Just(zu36000), app(app(ty_@2, bf), bg)) → new_esEs2(zu311000, zu36000, bf, bg)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, cc, app(app(ty_@2, ff), fg)) → new_esEs2(zu311002, zu36002, ff, fg)
new_esEs3(Left(zu311000), Left(zu36000), app(app(ty_@2, bbh), bca), gg) → new_esEs2(zu311000, zu36000, bbh, bca)
new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), gd, app(app(app(ty_@3, bac), bad), bae)) → new_esEs0(zu311001, zu36001, bac, bad, bae)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, cc, app(app(app(ty_@3, fa), fb), fc)) → new_esEs0(zu311002, zu36002, fa, fb, fc)
new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), gd, app(app(ty_Either, bba), bbb)) → new_esEs3(zu311001, zu36001, bba, bbb)
new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), app(ty_Maybe, gb)) → new_esEs(zu311010, zu36010, gb)
new_esEs3(Right(zu311000), Right(zu36000), gf, app(ty_[], bch)) → new_esEs1(zu311000, zu36000, bch)
new_esEs(Just(zu311000), Just(zu36000), app(ty_[], be)) → new_esEs1(zu311000, zu36000, be)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), app(app(ty_Either, dd), de), cc, cd) → new_esEs3(zu311000, zu36000, dd, de)
new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), app(app(app(ty_@3, hb), hc), hd), ge) → new_esEs0(zu311000, zu36000, hb, hc, hd)
new_esEs(Just(zu311000), Just(zu36000), app(app(ty_Either, bh), ca)) → new_esEs3(zu311000, zu36000, bh, ca)
new_esEs3(Right(zu311000), Right(zu36000), gf, app(ty_Maybe, bcd)) → new_esEs(zu311000, zu36000, bcd)
new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), app(app(app(ty_@3, df), cc), cd)) → new_esEs0(zu311010, zu36010, df, cc, cd)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, app(ty_Maybe, dg), cd) → new_esEs(zu311001, zu36001, dg)
new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), app(app(ty_@2, gd), ge)) → new_esEs2(zu311010, zu36010, gd, ge)
new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), gd, app(ty_[], baf)) → new_esEs1(zu311001, zu36001, baf)
new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), app(app(ty_Either, hh), baa), ge) → new_esEs3(zu311000, zu36000, hh, baa)
new_esEs3(Left(zu311000), Left(zu36000), app(ty_[], bbg), gg) → new_esEs1(zu311000, zu36000, bbg)
new_esEs3(Left(zu311000), Left(zu36000), app(ty_Maybe, bbc), gg) → new_esEs(zu311000, zu36000, bbc)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, cc, app(ty_Maybe, eh)) → new_esEs(zu311002, zu36002, eh)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, app(app(ty_Either, ef), eg), cd) → new_esEs3(zu311001, zu36001, ef, eg)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), app(ty_Maybe, cb), cc, cd) → new_esEs(zu311000, zu36000, cb)
new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), app(app(app(ty_@3, ce), cf), cg), cc, cd) → new_esEs0(zu311000, zu36000, ce, cf, cg)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), app(app(ty_Either, gf), gg)) → new_esEs3(zu311010, zu36010, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), app(app(app(ty_@3, df), cc), cd)) → new_esEs0(zu311010, zu36010, df, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), app(app(ty_@2, gd), ge)) → new_esEs2(zu311010, zu36010, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Just(zu311000), Just(zu36000), app(app(ty_Either, bh), ca)) → new_esEs3(zu311000, zu36000, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Just(zu311000), Just(zu36000), app(app(app(ty_@3, bb), bc), bd)) → new_esEs0(zu311000, zu36000, bb, bc, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(Just(zu311000), Just(zu36000), app(app(ty_@2, bf), bg)) → new_esEs2(zu311000, zu36000, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), app(ty_Maybe, gb)) → new_esEs(zu311010, zu36010, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Just(zu311000), Just(zu36000), app(ty_Maybe, ba)) → new_esEs(zu311000, zu36000, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Just(zu311000), Just(zu36000), app(ty_[], be)) → new_esEs1(zu311000, zu36000, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), gd, app(app(ty_Either, bba), bbb)) → new_esEs3(zu311001, zu36001, bba, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), app(app(ty_Either, hh), baa), ge) → new_esEs3(zu311000, zu36000, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), gd, app(app(app(ty_@3, bac), bad), bae)) → new_esEs0(zu311001, zu36001, bac, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), app(app(app(ty_@3, hb), hc), hd), ge) → new_esEs0(zu311000, zu36000, hb, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), gd, app(app(ty_@2, bag), bah)) → new_esEs2(zu311001, zu36001, bag, bah)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), app(app(ty_@2, hf), hg), ge) → new_esEs2(zu311000, zu36000, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), gd, app(ty_Maybe, bab)) → new_esEs(zu311001, zu36001, bab)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), app(ty_Maybe, ha), ge) → new_esEs(zu311000, zu36000, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), app(ty_[], he), ge) → new_esEs1(zu311000, zu36000, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(zu311000, zu311001), @2(zu36000, zu36001), gd, app(ty_[], baf)) → new_esEs1(zu311001, zu36001, baf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Right(zu311000), Right(zu36000), gf, app(app(ty_Either, bdc), bdd)) → new_esEs3(zu311000, zu36000, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(Left(zu311000), Left(zu36000), app(app(ty_Either, bcb), bcc), gg) → new_esEs3(zu311000, zu36000, bcb, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, cc, app(app(ty_Either, fh), ga)) → new_esEs3(zu311002, zu36002, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), app(app(ty_Either, dd), de), cc, cd) → new_esEs3(zu311000, zu36000, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, app(app(ty_Either, ef), eg), cd) → new_esEs3(zu311001, zu36001, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), gh) → new_esEs1(zu311011, zu36011, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs1(:(zu311010, zu311011), :(zu36010, zu36011), app(ty_[], gc)) → new_esEs1(zu311010, zu36010, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Right(zu311000), Right(zu36000), gf, app(app(app(ty_@3, bce), bcf), bcg)) → new_esEs0(zu311000, zu36000, bce, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(Left(zu311000), Left(zu36000), app(app(app(ty_@3, bbd), bbe), bbf), gg) → new_esEs0(zu311000, zu36000, bbd, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, app(app(app(ty_@3, dh), ea), eb), cd) → new_esEs0(zu311001, zu36001, dh, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, cc, app(app(app(ty_@3, fa), fb), fc)) → new_esEs0(zu311002, zu36002, fa, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), app(app(app(ty_@3, ce), cf), cg), cc, cd) → new_esEs0(zu311000, zu36000, ce, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Right(zu311000), Right(zu36000), gf, app(app(ty_@2, bda), bdb)) → new_esEs2(zu311000, zu36000, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(Left(zu311000), Left(zu36000), app(app(ty_@2, bbh), bca), gg) → new_esEs2(zu311000, zu36000, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Right(zu311000), Right(zu36000), gf, app(ty_Maybe, bcd)) → new_esEs(zu311000, zu36000, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Left(zu311000), Left(zu36000), app(ty_Maybe, bbc), gg) → new_esEs(zu311000, zu36000, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Right(zu311000), Right(zu36000), gf, app(ty_[], bch)) → new_esEs1(zu311000, zu36000, bch)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Left(zu311000), Left(zu36000), app(ty_[], bbg), gg) → new_esEs1(zu311000, zu36000, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, app(app(ty_@2, ed), ee), cd) → new_esEs2(zu311001, zu36001, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), app(app(ty_@2, db), dc), cc, cd) → new_esEs2(zu311000, zu36000, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, cc, app(app(ty_@2, ff), fg)) → new_esEs2(zu311002, zu36002, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, app(ty_Maybe, dg), cd) → new_esEs(zu311001, zu36001, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, cc, app(ty_Maybe, eh)) → new_esEs(zu311002, zu36002, eh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), app(ty_Maybe, cb), cc, cd) → new_esEs(zu311000, zu36000, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), app(ty_[], da), cc, cd) → new_esEs1(zu311000, zu36000, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, app(ty_[], ec), cd) → new_esEs1(zu311001, zu36001, ec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), df, cc, app(ty_[], fd)) → new_esEs1(zu311002, zu36002, fd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_nubByNubBy'1(zu176, zu177, zu178, zu179, False, :(zu1810, zu1811), ba) → new_nubByNubBy'1(zu176, zu177, zu178, zu179, new_esEs4(zu1810, zu176, ba), zu1811, ba)
new_nubByNubBy'1(zu176, zu177, zu178, zu179, False, [], ba) → new_nubByNubBy'(zu177, zu176, :(zu178, zu179), ba)
new_nubByNubBy'(:(zu840, zu841), zu85, zu86, bb) → new_nubByNubBy'1(zu840, zu841, zu85, zu86, new_esEs5(zu85, zu840, bb), zu86, bb)
new_nubByNubBy'1(zu176, zu177, zu178, zu179, True, zu181, ba) → new_nubByNubBy'(zu177, zu178, zu179, ba)
The TRS R consists of the following rules:
new_esEs19(Left(zu311000), Left(zu36000), ty_Ordering, bed) → new_esEs8(zu311000, zu36000)
new_esEs5(zu85, zu840, app(ty_Ratio, bdb)) → new_esEs10(zu85, zu840, bdb)
new_primPlusNat1(Succ(zu7000), Succ(zu36001000)) → Succ(Succ(new_primPlusNat1(zu7000, zu36001000)))
new_esEs24(zu311000, zu36000, ty_Char) → new_esEs15(zu311000, zu36000)
new_primEqInt(Neg(Succ(zu3110000)), Pos(zu36000)) → False
new_primEqInt(Pos(Succ(zu3110000)), Neg(zu36000)) → False
new_esEs23(zu311001, zu36001, app(app(ty_@2, fb), fc)) → new_esEs18(zu311001, zu36001, fb, fc)
new_esEs6(Just(zu311000), Just(zu36000), ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Double) → new_esEs14(zu311002, zu36002)
new_esEs26(zu311002, zu36002, ty_Int) → new_esEs9(zu311002, zu36002)
new_primEqInt(Neg(Zero), Pos(Succ(zu360000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(zu360000))) → False
new_esEs26(zu311002, zu36002, app(ty_[], bce)) → new_esEs17(zu311002, zu36002, bce)
new_esEs4(zu1810, zu176, app(app(app(ty_@3, ga), gb), gc)) → new_esEs13(zu1810, zu176, ga, gb, gc)
new_esEs19(Right(zu311000), Right(zu36000), bfg, app(ty_Maybe, bga)) → new_esEs6(zu311000, zu36000, bga)
new_esEs4(zu1810, zu176, app(app(ty_Either, gg), gh)) → new_esEs19(zu1810, zu176, gg, gh)
new_esEs23(zu311001, zu36001, app(ty_Ratio, ed)) → new_esEs10(zu311001, zu36001, ed)
new_esEs20(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs23(zu311001, zu36001, app(ty_[], fa)) → new_esEs17(zu311001, zu36001, fa)
new_esEs8(EQ, GT) → False
new_esEs8(GT, EQ) → False
new_esEs19(Left(zu311000), Left(zu36000), ty_@0, bed) → new_esEs12(zu311000, zu36000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs6(Just(zu311000), Just(zu36000), ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs4(zu1810, zu176, app(ty_[], gd)) → new_esEs17(zu1810, zu176, gd)
new_esEs19(Right(zu311000), Right(zu36000), bfg, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs26(zu311002, zu36002, app(ty_Ratio, bbh)) → new_esEs10(zu311002, zu36002, bbh)
new_esEs19(Right(zu311000), Right(zu36000), bfg, ty_Char) → new_esEs15(zu311000, zu36000)
new_esEs23(zu311001, zu36001, ty_Float) → new_esEs11(zu311001, zu36001)
new_esEs4(zu1810, zu176, ty_Ordering) → new_esEs8(zu1810, zu176)
new_esEs4(zu1810, zu176, app(ty_Maybe, fh)) → new_esEs6(zu1810, zu176, fh)
new_esEs19(Left(zu311000), Left(zu36000), app(app(ty_Either, bfe), bff), bed) → new_esEs19(zu311000, zu36000, bfe, bff)
new_primPlusNat0(Zero, zu3600100) → Succ(zu3600100)
new_esEs22(zu311000, zu36000, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs6(Just(zu311000), Just(zu36000), ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Char) → new_esEs15(zu311002, zu36002)
new_esEs5(zu85, zu840, ty_Float) → new_esEs11(zu85, zu840)
new_esEs5(zu85, zu840, app(ty_Maybe, bdc)) → new_esEs6(zu85, zu840, bdc)
new_sr(Neg(zu3110010), Pos(zu360010)) → Neg(new_primMulNat0(zu3110010, zu360010))
new_sr(Pos(zu3110010), Neg(zu360010)) → Neg(new_primMulNat0(zu3110010, zu360010))
new_esEs23(zu311001, zu36001, ty_Char) → new_esEs15(zu311001, zu36001)
new_esEs27(zu311010, zu36010, app(app(ty_@2, cg), da)) → new_esEs18(zu311010, zu36010, cg, da)
new_esEs24(zu311000, zu36000, app(ty_[], baa)) → new_esEs17(zu311000, zu36000, baa)
new_esEs24(zu311000, zu36000, app(app(ty_Either, bad), bae)) → new_esEs19(zu311000, zu36000, bad, bae)
new_esEs27(zu311010, zu36010, ty_Char) → new_esEs15(zu311010, zu36010)
new_esEs18(@2(zu311000, zu311001), @2(zu36000, zu36001), cg, da) → new_asAs(new_esEs22(zu311000, zu36000, cg), new_esEs23(zu311001, zu36001, da))
new_esEs21(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs22(zu311000, zu36000, app(ty_Maybe, dc)) → new_esEs6(zu311000, zu36000, dc)
new_esEs4(zu1810, zu176, ty_Float) → new_esEs11(zu1810, zu176)
new_esEs27(zu311010, zu36010, app(ty_Maybe, bc)) → new_esEs6(zu311010, zu36010, bc)
new_esEs26(zu311002, zu36002, app(app(ty_@2, bcf), bcg)) → new_esEs18(zu311002, zu36002, bcf, bcg)
new_esEs12(@0, @0) → True
new_esEs25(zu311001, zu36001, ty_Double) → new_esEs14(zu311001, zu36001)
new_esEs22(zu311000, zu36000, app(app(ty_Either, eb), ec)) → new_esEs19(zu311000, zu36000, eb, ec)
new_esEs24(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs22(zu311000, zu36000, app(app(ty_@2, dh), ea)) → new_esEs18(zu311000, zu36000, dh, ea)
new_esEs27(zu311010, zu36010, ty_Double) → new_esEs14(zu311010, zu36010)
new_primEqNat0(Zero, Succ(zu360000)) → False
new_primEqNat0(Succ(zu3110000), Zero) → False
new_esEs21(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(app(ty_@2, bfc), bfd), bed) → new_esEs18(zu311000, zu36000, bfc, bfd)
new_esEs25(zu311001, zu36001, app(ty_Maybe, bag)) → new_esEs6(zu311001, zu36001, bag)
new_esEs19(Right(zu311000), Right(zu36000), bfg, ty_@0) → new_esEs12(zu311000, zu36000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(zu311000, zu36000, ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs27(zu311010, zu36010, ty_Float) → new_esEs11(zu311010, zu36010)
new_esEs14(Double(zu311000, zu311001), Double(zu36000, zu36001)) → new_esEs9(new_sr(zu311000, zu36000), new_sr(zu311001, zu36001))
new_esEs26(zu311002, zu36002, app(app(app(ty_@3, bcb), bcc), bcd)) → new_esEs13(zu311002, zu36002, bcb, bcc, bcd)
new_esEs22(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs5(zu85, zu840, app(app(app(ty_@3, bdd), bde), bdf)) → new_esEs13(zu85, zu840, bdd, bde, bdf)
new_esEs27(zu311010, zu36010, app(app(app(ty_@3, ha), hb), hc)) → new_esEs13(zu311010, zu36010, ha, hb, hc)
new_esEs7(False, False) → True
new_esEs27(zu311010, zu36010, ty_Integer) → new_esEs16(zu311010, zu36010)
new_esEs22(zu311000, zu36000, app(ty_[], dg)) → new_esEs17(zu311000, zu36000, dg)
new_esEs24(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs27(zu311010, zu36010, app(ty_Ratio, cf)) → new_esEs10(zu311010, zu36010, cf)
new_esEs25(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs4(zu1810, zu176, ty_Double) → new_esEs14(zu1810, zu176)
new_esEs25(zu311001, zu36001, ty_Bool) → new_esEs7(zu311001, zu36001)
new_esEs27(zu311010, zu36010, app(ty_[], bhc)) → new_esEs17(zu311010, zu36010, bhc)
new_esEs22(zu311000, zu36000, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), bfg, app(app(app(ty_@3, bgb), bgc), bgd)) → new_esEs13(zu311000, zu36000, bgb, bgc, bgd)
new_esEs27(zu311010, zu36010, ty_Int) → new_esEs9(zu311010, zu36010)
new_esEs4(zu1810, zu176, app(app(ty_@2, ge), gf)) → new_esEs18(zu1810, zu176, ge, gf)
new_esEs22(zu311000, zu36000, ty_@0) → new_esEs12(zu311000, zu36000)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_[], ca)) → new_esEs17(zu311000, zu36000, ca)
new_esEs23(zu311001, zu36001, ty_Double) → new_esEs14(zu311001, zu36001)
new_esEs6(Just(zu311000), Just(zu36000), app(app(app(ty_@3, bf), bg), bh)) → new_esEs13(zu311000, zu36000, bf, bg, bh)
new_esEs16(Integer(zu311000), Integer(zu36000)) → new_primEqInt(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), bfg, app(ty_Ratio, bfh)) → new_esEs10(zu311000, zu36000, bfh)
new_esEs19(Right(zu311000), Right(zu36000), bfg, app(app(ty_Either, bgh), bha)) → new_esEs19(zu311000, zu36000, bgh, bha)
new_esEs25(zu311001, zu36001, ty_@0) → new_esEs12(zu311001, zu36001)
new_esEs4(zu1810, zu176, ty_Integer) → new_esEs16(zu1810, zu176)
new_esEs26(zu311002, zu36002, ty_Bool) → new_esEs7(zu311002, zu36002)
new_esEs8(LT, LT) → True
new_esEs5(zu85, zu840, ty_Char) → new_esEs15(zu85, zu840)
new_esEs25(zu311001, zu36001, ty_Ordering) → new_esEs8(zu311001, zu36001)
new_sr(Neg(zu3110010), Neg(zu360010)) → Pos(new_primMulNat0(zu3110010, zu360010))
new_esEs19(Right(zu311000), Right(zu36000), bfg, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs4(zu1810, zu176, app(ty_Ratio, fg)) → new_esEs10(zu1810, zu176, fg)
new_esEs25(zu311001, zu36001, app(app(ty_Either, bbf), bbg)) → new_esEs19(zu311001, zu36001, bbf, bbg)
new_sr(Pos(zu3110010), Pos(zu360010)) → Pos(new_primMulNat0(zu3110010, zu360010))
new_asAs(False, zu66) → False
new_primEqNat0(Zero, Zero) → True
new_esEs6(Just(zu311000), Just(zu36000), ty_Char) → new_esEs15(zu311000, zu36000)
new_primMulNat0(Zero, Succ(zu3600100)) → Zero
new_primMulNat0(Succ(zu31100100), Zero) → Zero
new_esEs19(Right(zu311000), Left(zu36000), bfg, bed) → False
new_esEs19(Left(zu311000), Right(zu36000), bfg, bed) → False
new_esEs26(zu311002, zu36002, app(ty_Maybe, bca)) → new_esEs6(zu311002, zu36002, bca)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_Maybe, be)) → new_esEs6(zu311000, zu36000, be)
new_esEs23(zu311001, zu36001, app(app(ty_Either, fd), ff)) → new_esEs19(zu311001, zu36001, fd, ff)
new_esEs19(Right(zu311000), Right(zu36000), bfg, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs4(zu1810, zu176, ty_Bool) → new_esEs7(zu1810, zu176)
new_esEs19(Right(zu311000), Right(zu36000), bfg, app(app(ty_@2, bgf), bgg)) → new_esEs18(zu311000, zu36000, bgf, bgg)
new_esEs6(Just(zu311000), Just(zu36000), ty_@0) → new_esEs12(zu311000, zu36000)
new_esEs23(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_Ratio, bee), bed) → new_esEs10(zu311000, zu36000, bee)
new_esEs23(zu311001, zu36001, app(app(app(ty_@3, ef), eg), eh)) → new_esEs13(zu311001, zu36001, ef, eg, eh)
new_esEs5(zu85, zu840, ty_Bool) → new_esEs7(zu85, zu840)
new_esEs6(Just(zu311000), Just(zu36000), ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs22(zu311000, zu36000, app(app(app(ty_@3, dd), de), df)) → new_esEs13(zu311000, zu36000, dd, de, df)
new_esEs17(:(zu311010, zu311011), :(zu36010, zu36011), bhb) → new_asAs(new_esEs27(zu311010, zu36010, bhb), new_esEs17(zu311011, zu36011, bhb))
new_esEs24(zu311000, zu36000, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs23(zu311001, zu36001, ty_Bool) → new_esEs7(zu311001, zu36001)
new_esEs23(zu311001, zu36001, app(ty_Maybe, ee)) → new_esEs6(zu311001, zu36001, ee)
new_esEs19(Right(zu311000), Right(zu36000), bfg, app(ty_[], bge)) → new_esEs17(zu311000, zu36000, bge)
new_esEs15(Char(zu311000), Char(zu36000)) → new_primEqNat0(zu311000, zu36000)
new_esEs25(zu311001, zu36001, app(ty_[], bbc)) → new_esEs17(zu311001, zu36001, bbc)
new_esEs19(Right(zu311000), Right(zu36000), bfg, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Ordering) → new_esEs8(zu311002, zu36002)
new_esEs4(zu1810, zu176, ty_@0) → new_esEs12(zu1810, zu176)
new_esEs24(zu311000, zu36000, app(ty_Ratio, hd)) → new_esEs10(zu311000, zu36000, hd)
new_esEs8(GT, GT) → True
new_esEs5(zu85, zu840, ty_Int) → new_esEs9(zu85, zu840)
new_primPlusNat0(Succ(zu700), zu3600100) → Succ(Succ(new_primPlusNat1(zu700, zu3600100)))
new_esEs26(zu311002, zu36002, ty_Float) → new_esEs11(zu311002, zu36002)
new_esEs23(zu311001, zu36001, ty_@0) → new_esEs12(zu311001, zu36001)
new_esEs8(LT, GT) → False
new_esEs8(GT, LT) → False
new_esEs22(zu311000, zu36000, app(ty_Ratio, db)) → new_esEs10(zu311000, zu36000, db)
new_esEs19(Left(zu311000), Left(zu36000), ty_Double, bed) → new_esEs14(zu311000, zu36000)
new_esEs25(zu311001, zu36001, app(app(app(ty_@3, bah), bba), bbb)) → new_esEs13(zu311001, zu36001, bah, bba, bbb)
new_primEqInt(Neg(Succ(zu3110000)), Neg(Succ(zu360000))) → new_primEqNat0(zu3110000, zu360000)
new_esEs26(zu311002, zu36002, app(app(ty_Either, bch), bda)) → new_esEs19(zu311002, zu36002, bch, bda)
new_esEs23(zu311001, zu36001, ty_Ordering) → new_esEs8(zu311001, zu36001)
new_esEs25(zu311001, zu36001, app(app(ty_@2, bbd), bbe)) → new_esEs18(zu311001, zu36001, bbd, bbe)
new_esEs24(zu311000, zu36000, app(app(ty_@2, bab), bac)) → new_esEs18(zu311000, zu36000, bab, bac)
new_primPlusNat1(Zero, Succ(zu36001000)) → Succ(zu36001000)
new_primPlusNat1(Succ(zu7000), Zero) → Succ(zu7000)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_Ratio, bd)) → new_esEs10(zu311000, zu36000, bd)
new_esEs25(zu311001, zu36001, ty_Char) → new_esEs15(zu311001, zu36001)
new_esEs25(zu311001, zu36001, app(ty_Ratio, baf)) → new_esEs10(zu311001, zu36001, baf)
new_esEs5(zu85, zu840, ty_@0) → new_esEs12(zu85, zu840)
new_esEs7(True, True) → True
new_esEs5(zu85, zu840, ty_Integer) → new_esEs16(zu85, zu840)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs6(Just(zu311000), Just(zu36000), ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs22(zu311000, zu36000, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs24(zu311000, zu36000, app(app(app(ty_@3, hf), hg), hh)) → new_esEs13(zu311000, zu36000, hf, hg, hh)
new_esEs4(zu1810, zu176, ty_Char) → new_esEs15(zu1810, zu176)
new_esEs22(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_[], bfb), bed) → new_esEs17(zu311000, zu36000, bfb)
new_primEqInt(Neg(Zero), Neg(Succ(zu360000))) → False
new_primEqInt(Neg(Succ(zu3110000)), Neg(Zero)) → False
new_esEs6(Just(zu311000), Just(zu36000), app(app(ty_@2, cb), cc)) → new_esEs18(zu311000, zu36000, cb, cc)
new_esEs8(EQ, EQ) → True
new_esEs7(True, False) → False
new_esEs7(False, True) → False
new_esEs23(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs5(zu85, zu840, ty_Double) → new_esEs14(zu85, zu840)
new_esEs19(Left(zu311000), Left(zu36000), ty_Char, bed) → new_esEs15(zu311000, zu36000)
new_esEs20(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs19(Left(zu311000), Left(zu36000), app(app(app(ty_@3, beg), beh), bfa), bed) → new_esEs13(zu311000, zu36000, beg, beh, bfa)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs10(:%(zu311000, zu311001), :%(zu36000, zu36001), cf) → new_asAs(new_esEs20(zu311000, zu36000, cf), new_esEs21(zu311001, zu36001, cf))
new_asAs(True, zu66) → zu66
new_esEs27(zu311010, zu36010, ty_Bool) → new_esEs7(zu311010, zu36010)
new_esEs19(Left(zu311000), Left(zu36000), ty_Int, bed) → new_esEs9(zu311000, zu36000)
new_primMulNat0(Succ(zu31100100), Succ(zu3600100)) → new_primPlusNat0(new_primMulNat0(zu31100100, Succ(zu3600100)), zu3600100)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_Maybe, bef), bed) → new_esEs6(zu311000, zu36000, bef)
new_esEs27(zu311010, zu36010, app(app(ty_Either, bfg), bed)) → new_esEs19(zu311010, zu36010, bfg, bed)
new_esEs25(zu311001, zu36001, ty_Float) → new_esEs11(zu311001, zu36001)
new_esEs26(zu311002, zu36002, ty_Integer) → new_esEs16(zu311002, zu36002)
new_esEs6(Nothing, Nothing, bc) → True
new_esEs19(Left(zu311000), Left(zu36000), ty_Float, bed) → new_esEs11(zu311000, zu36000)
new_esEs5(zu85, zu840, app(app(ty_Either, beb), bec)) → new_esEs19(zu85, zu840, beb, bec)
new_primEqInt(Pos(Succ(zu3110000)), Pos(Succ(zu360000))) → new_primEqNat0(zu3110000, zu360000)
new_esEs17([], [], bhb) → True
new_esEs17(:(zu311010, zu311011), [], bhb) → False
new_esEs17([], :(zu36010, zu36011), bhb) → False
new_esEs25(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs5(zu85, zu840, app(ty_[], bdg)) → new_esEs17(zu85, zu840, bdg)
new_esEs5(zu85, zu840, ty_Ordering) → new_esEs8(zu85, zu840)
new_esEs11(Float(zu311000, zu311001), Float(zu36000, zu36001)) → new_esEs9(new_sr(zu311000, zu36000), new_sr(zu311001, zu36001))
new_esEs6(Just(zu311000), Nothing, bc) → False
new_esEs6(Nothing, Just(zu36000), bc) → False
new_primEqNat0(Succ(zu3110000), Succ(zu360000)) → new_primEqNat0(zu3110000, zu360000)
new_esEs9(zu31100, zu3600) → new_primEqInt(zu31100, zu3600)
new_esEs27(zu311010, zu36010, ty_Ordering) → new_esEs8(zu311010, zu36010)
new_esEs27(zu311010, zu36010, ty_@0) → new_esEs12(zu311010, zu36010)
new_esEs6(Just(zu311000), Just(zu36000), app(app(ty_Either, cd), ce)) → new_esEs19(zu311000, zu36000, cd, ce)
new_esEs19(Left(zu311000), Left(zu36000), ty_Integer, bed) → new_esEs16(zu311000, zu36000)
new_esEs24(zu311000, zu36000, app(ty_Maybe, he)) → new_esEs6(zu311000, zu36000, he)
new_esEs13(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), ha, hb, hc) → new_asAs(new_esEs24(zu311000, zu36000, ha), new_asAs(new_esEs25(zu311001, zu36001, hb), new_esEs26(zu311002, zu36002, hc)))
new_esEs26(zu311002, zu36002, ty_@0) → new_esEs12(zu311002, zu36002)
new_esEs4(zu1810, zu176, ty_Int) → new_esEs9(zu1810, zu176)
new_esEs24(zu311000, zu36000, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs5(zu85, zu840, app(app(ty_@2, bdh), bea)) → new_esEs18(zu85, zu840, bdh, bea)
new_esEs19(Right(zu311000), Right(zu36000), bfg, ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs22(zu311000, zu36000, ty_Char) → new_esEs15(zu311000, zu36000)
new_esEs6(Just(zu311000), Just(zu36000), ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs8(LT, EQ) → False
new_esEs8(EQ, LT) → False
new_primEqInt(Pos(Succ(zu3110000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(zu360000))) → False
new_esEs19(Left(zu311000), Left(zu36000), ty_Bool, bed) → new_esEs7(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_@0) → new_esEs12(zu311000, zu36000)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs19(Right(zu311000), Right(zu36000), bfg, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_Double) → new_esEs14(zu311000, zu36000)
The set Q consists of the following terms:
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Integer)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs5(x0, x1, ty_Float)
new_primPlusNat1(Zero, Succ(x0))
new_esEs27(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_@0)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Int)
new_esEs5(x0, x1, ty_@0)
new_esEs26(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Nothing, Just(x0), x1)
new_esEs4(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, ty_Char)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_esEs5(x0, x1, ty_Ordering)
new_esEs7(False, False)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(EQ, EQ)
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_sr(Pos(x0), Pos(x1))
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Char)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs26(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_Bool)
new_asAs(False, x0)
new_esEs8(GT, GT)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Ordering)
new_esEs27(x0, x1, ty_Bool)
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Double)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_esEs23(x0, x1, ty_Double)
new_esEs8(LT, LT)
new_esEs7(False, True)
new_esEs7(True, False)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs15(Char(x0), Char(x1))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs22(x0, x1, ty_Float)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Ordering)
new_esEs8(EQ, GT)
new_esEs8(GT, EQ)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs21(x0, x1, ty_Integer)
new_asAs(True, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs8(GT, LT)
new_esEs8(LT, GT)
new_esEs4(x0, x1, ty_Float)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Nothing, x1)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs24(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_sr(Neg(x0), Neg(x1))
new_primEqNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), x1)
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs23(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs4(x0, x1, ty_Double)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Int)
new_esEs25(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Integer)
new_esEs12(@0, @0)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Zero, Zero)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs5(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs9(x0, x1)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs6(Nothing, Nothing, x0)
new_esEs22(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs23(x0, x1, ty_Ordering)
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, ty_Float)
new_esEs7(True, True)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs17([], :(x0, x1), x2)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs26(x0, x1, ty_Float)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17([], [], x0)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs16(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Char)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs24(x0, x1, ty_Double)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqNat0(Zero, Succ(x0))
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs5(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_@0)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs8(LT, EQ)
new_esEs8(EQ, LT)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs23(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs25(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_@0)
new_esEs27(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_esEs27(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs5(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Bool)
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs23(x0, x1, ty_Float)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(:(x0, x1), [], x2)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Float)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Zero)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_nubByNubBy'1(zu176, zu177, zu178, zu179, False, :(zu1810, zu1811), ba) → new_nubByNubBy'1(zu176, zu177, zu178, zu179, new_esEs4(zu1810, zu176, ba), zu1811, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 6 > 6, 7 >= 7
- new_nubByNubBy'(:(zu840, zu841), zu85, zu86, bb) → new_nubByNubBy'1(zu840, zu841, zu85, zu86, new_esEs5(zu85, zu840, bb), zu86, bb)
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 3, 3 >= 4, 3 >= 6, 4 >= 7
- new_nubByNubBy'1(zu176, zu177, zu178, zu179, False, [], ba) → new_nubByNubBy'(zu177, zu176, :(zu178, zu179), ba)
The graph contains the following edges 2 >= 1, 1 >= 2, 7 >= 4
- new_nubByNubBy'1(zu176, zu177, zu178, zu179, True, zu181, ba) → new_nubByNubBy'(zu177, zu178, zu179, ba)
The graph contains the following edges 2 >= 1, 3 >= 2, 4 >= 3, 7 >= 4
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy([], :(:(zu3600, zu3601), zu361), bb) → new_deleteBy([], zu361, bb)
new_deleteBy0(zu45, zu46, zu47, zu48, zu49, False, ba) → new_deleteBy(:(zu48, zu49), zu45, ba)
new_deleteBy(:(zu31100, zu31101), :([], zu361), bb) → new_deleteBy(:(zu31100, zu31101), zu361, bb)
new_deleteBy(:(zu31100, zu31101), :(:(zu3600, zu3601), zu361), bb) → new_deleteBy0(zu361, zu3600, zu3601, zu31100, zu31101, new_asAs(new_esEs28(zu31100, zu3600, bb), new_esEs17(zu31101, zu3601, bb)), bb)
The TRS R consists of the following rules:
new_esEs19(Left(zu311000), Left(zu36000), ty_Ordering, dg) → new_esEs8(zu311000, zu36000)
new_primPlusNat1(Succ(zu7000), Succ(zu36001000)) → Succ(Succ(new_primPlusNat1(zu7000, zu36001000)))
new_esEs24(zu311000, zu36000, ty_Char) → new_esEs15(zu311000, zu36000)
new_primEqInt(Neg(Succ(zu3110000)), Pos(zu36000)) → False
new_primEqInt(Pos(Succ(zu3110000)), Neg(zu36000)) → False
new_esEs23(zu311001, zu36001, app(app(ty_@2, ga), gb)) → new_esEs18(zu311001, zu36001, ga, gb)
new_esEs6(Just(zu311000), Just(zu36000), ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Double) → new_esEs14(zu311002, zu36002)
new_esEs26(zu311002, zu36002, ty_Int) → new_esEs9(zu311002, zu36002)
new_esEs28(zu31100, zu3600, app(ty_Maybe, bc)) → new_esEs6(zu31100, zu3600, bc)
new_primEqInt(Neg(Zero), Pos(Succ(zu360000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(zu360000))) → False
new_esEs26(zu311002, zu36002, app(ty_[], bbf)) → new_esEs17(zu311002, zu36002, bbf)
new_esEs19(Right(zu311000), Right(zu36000), df, app(ty_Maybe, bdf)) → new_esEs6(zu311000, zu36000, bdf)
new_esEs23(zu311001, zu36001, app(ty_Ratio, fb)) → new_esEs10(zu311001, zu36001, fb)
new_esEs20(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs23(zu311001, zu36001, app(ty_[], fh)) → new_esEs17(zu311001, zu36001, fh)
new_esEs8(EQ, GT) → False
new_esEs8(GT, EQ) → False
new_esEs19(Left(zu311000), Left(zu36000), ty_@0, dg) → new_esEs12(zu311000, zu36000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs6(Just(zu311000), Just(zu36000), ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs26(zu311002, zu36002, app(ty_Ratio, bba)) → new_esEs10(zu311002, zu36002, bba)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Char) → new_esEs15(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(ty_Ratio, cf)) → new_esEs10(zu31100, zu3600, cf)
new_esEs23(zu311001, zu36001, ty_Float) → new_esEs11(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(app(ty_Either, bdc), bdd), dg) → new_esEs19(zu311000, zu36000, bdc, bdd)
new_primPlusNat0(Zero, zu3600100) → Succ(zu3600100)
new_esEs22(zu311000, zu36000, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(app(app(ty_@3, cg), da), db)) → new_esEs13(zu31100, zu3600, cg, da, db)
new_esEs6(Just(zu311000), Just(zu36000), ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Char) → new_esEs15(zu311002, zu36002)
new_sr(Neg(zu3110010), Pos(zu360010)) → Neg(new_primMulNat0(zu3110010, zu360010))
new_sr(Pos(zu3110010), Neg(zu360010)) → Neg(new_primMulNat0(zu3110010, zu360010))
new_esEs23(zu311001, zu36001, ty_Char) → new_esEs15(zu311001, zu36001)
new_esEs27(zu311010, zu36010, app(app(ty_@2, dd), de)) → new_esEs18(zu311010, zu36010, dd, de)
new_esEs24(zu311000, zu36000, app(ty_[], hb)) → new_esEs17(zu311000, zu36000, hb)
new_esEs24(zu311000, zu36000, app(app(ty_Either, he), hf)) → new_esEs19(zu311000, zu36000, he, hf)
new_esEs27(zu311010, zu36010, ty_Char) → new_esEs15(zu311010, zu36010)
new_esEs18(@2(zu311000, zu311001), @2(zu36000, zu36001), dd, de) → new_asAs(new_esEs22(zu311000, zu36000, dd), new_esEs23(zu311001, zu36001, de))
new_esEs21(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs22(zu311000, zu36000, app(ty_Maybe, ea)) → new_esEs6(zu311000, zu36000, ea)
new_esEs27(zu311010, zu36010, app(ty_Maybe, bc)) → new_esEs6(zu311010, zu36010, bc)
new_esEs26(zu311002, zu36002, app(app(ty_@2, bbg), bbh)) → new_esEs18(zu311002, zu36002, bbg, bbh)
new_esEs12(@0, @0) → True
new_esEs25(zu311001, zu36001, ty_Double) → new_esEs14(zu311001, zu36001)
new_esEs28(zu31100, zu3600, ty_@0) → new_esEs12(zu31100, zu3600)
new_esEs22(zu311000, zu36000, app(app(ty_Either, eh), fa)) → new_esEs19(zu311000, zu36000, eh, fa)
new_esEs24(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Double) → new_esEs14(zu31100, zu3600)
new_esEs22(zu311000, zu36000, app(app(ty_@2, ef), eg)) → new_esEs18(zu311000, zu36000, ef, eg)
new_esEs27(zu311010, zu36010, ty_Double) → new_esEs14(zu311010, zu36010)
new_primEqNat0(Succ(zu3110000), Zero) → False
new_primEqNat0(Zero, Succ(zu360000)) → False
new_esEs21(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(app(ty_@2, bda), bdb), dg) → new_esEs18(zu311000, zu36000, bda, bdb)
new_esEs25(zu311001, zu36001, app(ty_Maybe, hh)) → new_esEs6(zu311001, zu36001, hh)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_@0) → new_esEs12(zu311000, zu36000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(zu311000, zu36000, ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs27(zu311010, zu36010, ty_Float) → new_esEs11(zu311010, zu36010)
new_esEs14(Double(zu311000, zu311001), Double(zu36000, zu36001)) → new_esEs9(new_sr(zu311000, zu36000), new_sr(zu311001, zu36001))
new_esEs26(zu311002, zu36002, app(app(app(ty_@3, bbc), bbd), bbe)) → new_esEs13(zu311002, zu36002, bbc, bbd, bbe)
new_esEs22(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs27(zu311010, zu36010, app(app(app(ty_@3, cg), da), db)) → new_esEs13(zu311010, zu36010, cg, da, db)
new_esEs7(False, False) → True
new_esEs27(zu311010, zu36010, ty_Integer) → new_esEs16(zu311010, zu36010)
new_esEs22(zu311000, zu36000, app(ty_[], ee)) → new_esEs17(zu311000, zu36000, ee)
new_esEs27(zu311010, zu36010, app(ty_Ratio, cf)) → new_esEs10(zu311010, zu36010, cf)
new_esEs24(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs25(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs25(zu311001, zu36001, ty_Bool) → new_esEs7(zu311001, zu36001)
new_esEs27(zu311010, zu36010, app(ty_[], dc)) → new_esEs17(zu311010, zu36010, dc)
new_esEs22(zu311000, zu36000, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, app(app(app(ty_@3, bdg), bdh), bea)) → new_esEs13(zu311000, zu36000, bdg, bdh, bea)
new_esEs27(zu311010, zu36010, ty_Int) → new_esEs9(zu311010, zu36010)
new_esEs22(zu311000, zu36000, ty_@0) → new_esEs12(zu311000, zu36000)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_[], ca)) → new_esEs17(zu311000, zu36000, ca)
new_esEs23(zu311001, zu36001, ty_Double) → new_esEs14(zu311001, zu36001)
new_esEs6(Just(zu311000), Just(zu36000), app(app(app(ty_@3, bf), bg), bh)) → new_esEs13(zu311000, zu36000, bf, bg, bh)
new_esEs16(Integer(zu311000), Integer(zu36000)) → new_primEqInt(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, app(ty_Ratio, bde)) → new_esEs10(zu311000, zu36000, bde)
new_esEs19(Right(zu311000), Right(zu36000), df, app(app(ty_Either, bee), bef)) → new_esEs19(zu311000, zu36000, bee, bef)
new_esEs25(zu311001, zu36001, ty_@0) → new_esEs12(zu311001, zu36001)
new_esEs26(zu311002, zu36002, ty_Bool) → new_esEs7(zu311002, zu36002)
new_esEs8(LT, LT) → True
new_sr(Neg(zu3110010), Neg(zu360010)) → Pos(new_primMulNat0(zu3110010, zu360010))
new_esEs25(zu311001, zu36001, ty_Ordering) → new_esEs8(zu311001, zu36001)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs25(zu311001, zu36001, app(app(ty_Either, bag), bah)) → new_esEs19(zu311001, zu36001, bag, bah)
new_esEs28(zu31100, zu3600, ty_Integer) → new_esEs16(zu31100, zu3600)
new_sr(Pos(zu3110010), Pos(zu360010)) → Pos(new_primMulNat0(zu3110010, zu360010))
new_asAs(False, zu66) → False
new_primEqNat0(Zero, Zero) → True
new_esEs6(Just(zu311000), Just(zu36000), ty_Char) → new_esEs15(zu311000, zu36000)
new_primMulNat0(Zero, Succ(zu3600100)) → Zero
new_primMulNat0(Succ(zu31100100), Zero) → Zero
new_esEs19(Right(zu311000), Left(zu36000), df, dg) → False
new_esEs19(Left(zu311000), Right(zu36000), df, dg) → False
new_esEs26(zu311002, zu36002, app(ty_Maybe, bbb)) → new_esEs6(zu311002, zu36002, bbb)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_Maybe, be)) → new_esEs6(zu311000, zu36000, be)
new_esEs23(zu311001, zu36001, app(app(ty_Either, gc), gd)) → new_esEs19(zu311001, zu36001, gc, gd)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(app(ty_Either, df), dg)) → new_esEs19(zu31100, zu3600, df, dg)
new_esEs19(Right(zu311000), Right(zu36000), df, app(app(ty_@2, bec), bed)) → new_esEs18(zu311000, zu36000, bec, bed)
new_esEs6(Just(zu311000), Just(zu36000), ty_@0) → new_esEs12(zu311000, zu36000)
new_esEs23(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_Ratio, bcc), dg) → new_esEs10(zu311000, zu36000, bcc)
new_esEs23(zu311001, zu36001, app(app(app(ty_@3, fd), ff), fg)) → new_esEs13(zu311001, zu36001, fd, ff, fg)
new_esEs17(:(zu311010, zu311011), :(zu36010, zu36011), bb) → new_asAs(new_esEs27(zu311010, zu36010, bb), new_esEs17(zu311011, zu36011, bb))
new_esEs6(Just(zu311000), Just(zu36000), ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs22(zu311000, zu36000, app(app(app(ty_@3, eb), ec), ed)) → new_esEs13(zu311000, zu36000, eb, ec, ed)
new_esEs24(zu311000, zu36000, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Bool) → new_esEs7(zu31100, zu3600)
new_esEs23(zu311001, zu36001, ty_Bool) → new_esEs7(zu311001, zu36001)
new_esEs23(zu311001, zu36001, app(ty_Maybe, fc)) → new_esEs6(zu311001, zu36001, fc)
new_esEs19(Right(zu311000), Right(zu36000), df, app(ty_[], beb)) → new_esEs17(zu311000, zu36000, beb)
new_esEs15(Char(zu311000), Char(zu36000)) → new_primEqNat0(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(app(ty_@2, dd), de)) → new_esEs18(zu31100, zu3600, dd, de)
new_esEs25(zu311001, zu36001, app(ty_[], bad)) → new_esEs17(zu311001, zu36001, bad)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Ordering) → new_esEs8(zu311002, zu36002)
new_esEs24(zu311000, zu36000, app(ty_Ratio, ge)) → new_esEs10(zu311000, zu36000, ge)
new_esEs8(GT, GT) → True
new_primPlusNat0(Succ(zu700), zu3600100) → Succ(Succ(new_primPlusNat1(zu700, zu3600100)))
new_esEs26(zu311002, zu36002, ty_Float) → new_esEs11(zu311002, zu36002)
new_esEs23(zu311001, zu36001, ty_@0) → new_esEs12(zu311001, zu36001)
new_esEs8(LT, GT) → False
new_esEs8(GT, LT) → False
new_esEs22(zu311000, zu36000, app(ty_Ratio, dh)) → new_esEs10(zu311000, zu36000, dh)
new_esEs19(Left(zu311000), Left(zu36000), ty_Double, dg) → new_esEs14(zu311000, zu36000)
new_esEs25(zu311001, zu36001, app(app(app(ty_@3, baa), bab), bac)) → new_esEs13(zu311001, zu36001, baa, bab, bac)
new_primEqInt(Neg(Succ(zu3110000)), Neg(Succ(zu360000))) → new_primEqNat0(zu3110000, zu360000)
new_esEs28(zu31100, zu3600, app(ty_[], dc)) → new_esEs17(zu31100, zu3600, dc)
new_esEs26(zu311002, zu36002, app(app(ty_Either, bca), bcb)) → new_esEs19(zu311002, zu36002, bca, bcb)
new_esEs23(zu311001, zu36001, ty_Ordering) → new_esEs8(zu311001, zu36001)
new_esEs25(zu311001, zu36001, app(app(ty_@2, bae), baf)) → new_esEs18(zu311001, zu36001, bae, baf)
new_esEs24(zu311000, zu36000, app(app(ty_@2, hc), hd)) → new_esEs18(zu311000, zu36000, hc, hd)
new_esEs28(zu31100, zu3600, ty_Char) → new_esEs15(zu31100, zu3600)
new_primPlusNat1(Zero, Succ(zu36001000)) → Succ(zu36001000)
new_primPlusNat1(Succ(zu7000), Zero) → Succ(zu7000)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_Ratio, bd)) → new_esEs10(zu311000, zu36000, bd)
new_esEs25(zu311001, zu36001, ty_Char) → new_esEs15(zu311001, zu36001)
new_esEs25(zu311001, zu36001, app(ty_Ratio, hg)) → new_esEs10(zu311001, zu36001, hg)
new_esEs7(True, True) → True
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs6(Just(zu311000), Just(zu36000), ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs22(zu311000, zu36000, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs24(zu311000, zu36000, app(app(app(ty_@3, gg), gh), ha)) → new_esEs13(zu311000, zu36000, gg, gh, ha)
new_esEs28(zu31100, zu3600, ty_Float) → new_esEs11(zu31100, zu3600)
new_esEs28(zu31100, zu3600, ty_Int) → new_esEs9(zu31100, zu3600)
new_esEs22(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_[], bch), dg) → new_esEs17(zu311000, zu36000, bch)
new_primEqInt(Neg(Zero), Neg(Succ(zu360000))) → False
new_primEqInt(Neg(Succ(zu3110000)), Neg(Zero)) → False
new_esEs6(Just(zu311000), Just(zu36000), app(app(ty_@2, cb), cc)) → new_esEs18(zu311000, zu36000, cb, cc)
new_esEs8(EQ, EQ) → True
new_esEs7(False, True) → False
new_esEs7(True, False) → False
new_esEs23(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), ty_Char, dg) → new_esEs15(zu311000, zu36000)
new_esEs20(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs19(Left(zu311000), Left(zu36000), app(app(app(ty_@3, bce), bcf), bcg), dg) → new_esEs13(zu311000, zu36000, bce, bcf, bcg)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs10(:%(zu311000, zu311001), :%(zu36000, zu36001), cf) → new_asAs(new_esEs20(zu311000, zu36000, cf), new_esEs21(zu311001, zu36001, cf))
new_asAs(True, zu66) → zu66
new_esEs27(zu311010, zu36010, ty_Bool) → new_esEs7(zu311010, zu36010)
new_esEs19(Left(zu311000), Left(zu36000), ty_Int, dg) → new_esEs9(zu311000, zu36000)
new_primMulNat0(Succ(zu31100100), Succ(zu3600100)) → new_primPlusNat0(new_primMulNat0(zu31100100, Succ(zu3600100)), zu3600100)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_Maybe, bcd), dg) → new_esEs6(zu311000, zu36000, bcd)
new_esEs27(zu311010, zu36010, app(app(ty_Either, df), dg)) → new_esEs19(zu311010, zu36010, df, dg)
new_esEs25(zu311001, zu36001, ty_Float) → new_esEs11(zu311001, zu36001)
new_esEs26(zu311002, zu36002, ty_Integer) → new_esEs16(zu311002, zu36002)
new_esEs6(Nothing, Nothing, bc) → True
new_esEs19(Left(zu311000), Left(zu36000), ty_Float, dg) → new_esEs11(zu311000, zu36000)
new_primEqInt(Pos(Succ(zu3110000)), Pos(Succ(zu360000))) → new_primEqNat0(zu3110000, zu360000)
new_esEs17([], [], bb) → True
new_esEs17([], :(zu36010, zu36011), bb) → False
new_esEs17(:(zu311010, zu311011), [], bb) → False
new_esEs25(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs11(Float(zu311000, zu311001), Float(zu36000, zu36001)) → new_esEs9(new_sr(zu311000, zu36000), new_sr(zu311001, zu36001))
new_esEs6(Just(zu311000), Nothing, bc) → False
new_esEs6(Nothing, Just(zu36000), bc) → False
new_primEqNat0(Succ(zu3110000), Succ(zu360000)) → new_primEqNat0(zu3110000, zu360000)
new_esEs27(zu311010, zu36010, ty_@0) → new_esEs12(zu311010, zu36010)
new_esEs27(zu311010, zu36010, ty_Ordering) → new_esEs8(zu311010, zu36010)
new_esEs9(zu31100, zu3600) → new_primEqInt(zu31100, zu3600)
new_esEs6(Just(zu311000), Just(zu36000), app(app(ty_Either, cd), ce)) → new_esEs19(zu311000, zu36000, cd, ce)
new_esEs19(Left(zu311000), Left(zu36000), ty_Integer, dg) → new_esEs16(zu311000, zu36000)
new_esEs24(zu311000, zu36000, app(ty_Maybe, gf)) → new_esEs6(zu311000, zu36000, gf)
new_esEs13(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), cg, da, db) → new_asAs(new_esEs24(zu311000, zu36000, cg), new_asAs(new_esEs25(zu311001, zu36001, da), new_esEs26(zu311002, zu36002, db)))
new_esEs26(zu311002, zu36002, ty_@0) → new_esEs12(zu311002, zu36002)
new_esEs24(zu311000, zu36000, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs22(zu311000, zu36000, ty_Char) → new_esEs15(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Ordering) → new_esEs8(zu31100, zu3600)
new_esEs6(Just(zu311000), Just(zu36000), ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs8(LT, EQ) → False
new_esEs8(EQ, LT) → False
new_primEqInt(Pos(Succ(zu3110000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(zu360000))) → False
new_esEs19(Left(zu311000), Left(zu36000), ty_Bool, dg) → new_esEs7(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_@0) → new_esEs12(zu311000, zu36000)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_Double) → new_esEs14(zu311000, zu36000)
The set Q consists of the following terms:
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs28(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_@0)
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs20(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_esEs7(False, False)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs8(EQ, EQ)
new_sr(Pos(x0), Pos(x1))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Char)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(:(x0, x1), [], x2)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Integer)
new_asAs(False, x0)
new_esEs26(x0, x1, ty_Bool)
new_esEs8(GT, GT)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Ordering)
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Double)
new_esEs8(LT, LT)
new_esEs7(True, False)
new_esEs7(False, True)
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs15(Char(x0), Char(x1))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs8(EQ, GT)
new_esEs8(GT, EQ)
new_esEs28(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_asAs(True, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs28(x0, x1, ty_Char)
new_esEs8(GT, LT)
new_esEs8(LT, GT)
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Nothing, x1)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs24(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_primEqNat0(Zero, Zero)
new_sr(Neg(x0), Neg(x1))
new_primPlusNat0(Succ(x0), x1)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs23(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Int)
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(@0, @0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs28(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(x0, x1)
new_esEs28(x0, x1, ty_Bool)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs6(Nothing, Nothing, x0)
new_esEs22(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs7(True, True)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs28(x0, x1, ty_Int)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs26(x0, x1, ty_Float)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs16(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, ty_Char)
new_esEs28(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_@0)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs8(LT, EQ)
new_esEs8(EQ, LT)
new_esEs23(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_esEs27(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs23(x0, x1, ty_Float)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs6(Just(x0), Just(x1), ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Float)
new_esEs28(x0, x1, ty_@0)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs28(x0, x1, ty_Float)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17([], :(x0, x1), x2)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs27(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Zero)
new_esEs17([], [], x0)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy0(zu45, zu46, zu47, zu48, zu49, False, ba) → new_deleteBy(:(zu48, zu49), zu45, ba)
new_deleteBy(:(zu31100, zu31101), :([], zu361), bb) → new_deleteBy(:(zu31100, zu31101), zu361, bb)
new_deleteBy(:(zu31100, zu31101), :(:(zu3600, zu3601), zu361), bb) → new_deleteBy0(zu361, zu3600, zu3601, zu31100, zu31101, new_asAs(new_esEs28(zu31100, zu3600, bb), new_esEs17(zu31101, zu3601, bb)), bb)
The TRS R consists of the following rules:
new_esEs19(Left(zu311000), Left(zu36000), ty_Ordering, dg) → new_esEs8(zu311000, zu36000)
new_primPlusNat1(Succ(zu7000), Succ(zu36001000)) → Succ(Succ(new_primPlusNat1(zu7000, zu36001000)))
new_esEs24(zu311000, zu36000, ty_Char) → new_esEs15(zu311000, zu36000)
new_primEqInt(Neg(Succ(zu3110000)), Pos(zu36000)) → False
new_primEqInt(Pos(Succ(zu3110000)), Neg(zu36000)) → False
new_esEs23(zu311001, zu36001, app(app(ty_@2, ga), gb)) → new_esEs18(zu311001, zu36001, ga, gb)
new_esEs6(Just(zu311000), Just(zu36000), ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Double) → new_esEs14(zu311002, zu36002)
new_esEs26(zu311002, zu36002, ty_Int) → new_esEs9(zu311002, zu36002)
new_esEs28(zu31100, zu3600, app(ty_Maybe, bc)) → new_esEs6(zu31100, zu3600, bc)
new_primEqInt(Neg(Zero), Pos(Succ(zu360000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(zu360000))) → False
new_esEs26(zu311002, zu36002, app(ty_[], bbf)) → new_esEs17(zu311002, zu36002, bbf)
new_esEs19(Right(zu311000), Right(zu36000), df, app(ty_Maybe, bdf)) → new_esEs6(zu311000, zu36000, bdf)
new_esEs23(zu311001, zu36001, app(ty_Ratio, fb)) → new_esEs10(zu311001, zu36001, fb)
new_esEs20(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs23(zu311001, zu36001, app(ty_[], fh)) → new_esEs17(zu311001, zu36001, fh)
new_esEs8(EQ, GT) → False
new_esEs8(GT, EQ) → False
new_esEs19(Left(zu311000), Left(zu36000), ty_@0, dg) → new_esEs12(zu311000, zu36000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs6(Just(zu311000), Just(zu36000), ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs26(zu311002, zu36002, app(ty_Ratio, bba)) → new_esEs10(zu311002, zu36002, bba)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Char) → new_esEs15(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(ty_Ratio, cf)) → new_esEs10(zu31100, zu3600, cf)
new_esEs23(zu311001, zu36001, ty_Float) → new_esEs11(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(app(ty_Either, bdc), bdd), dg) → new_esEs19(zu311000, zu36000, bdc, bdd)
new_primPlusNat0(Zero, zu3600100) → Succ(zu3600100)
new_esEs22(zu311000, zu36000, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(app(app(ty_@3, cg), da), db)) → new_esEs13(zu31100, zu3600, cg, da, db)
new_esEs6(Just(zu311000), Just(zu36000), ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Char) → new_esEs15(zu311002, zu36002)
new_sr(Neg(zu3110010), Pos(zu360010)) → Neg(new_primMulNat0(zu3110010, zu360010))
new_sr(Pos(zu3110010), Neg(zu360010)) → Neg(new_primMulNat0(zu3110010, zu360010))
new_esEs23(zu311001, zu36001, ty_Char) → new_esEs15(zu311001, zu36001)
new_esEs27(zu311010, zu36010, app(app(ty_@2, dd), de)) → new_esEs18(zu311010, zu36010, dd, de)
new_esEs24(zu311000, zu36000, app(ty_[], hb)) → new_esEs17(zu311000, zu36000, hb)
new_esEs24(zu311000, zu36000, app(app(ty_Either, he), hf)) → new_esEs19(zu311000, zu36000, he, hf)
new_esEs27(zu311010, zu36010, ty_Char) → new_esEs15(zu311010, zu36010)
new_esEs18(@2(zu311000, zu311001), @2(zu36000, zu36001), dd, de) → new_asAs(new_esEs22(zu311000, zu36000, dd), new_esEs23(zu311001, zu36001, de))
new_esEs21(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs22(zu311000, zu36000, app(ty_Maybe, ea)) → new_esEs6(zu311000, zu36000, ea)
new_esEs27(zu311010, zu36010, app(ty_Maybe, bc)) → new_esEs6(zu311010, zu36010, bc)
new_esEs26(zu311002, zu36002, app(app(ty_@2, bbg), bbh)) → new_esEs18(zu311002, zu36002, bbg, bbh)
new_esEs12(@0, @0) → True
new_esEs25(zu311001, zu36001, ty_Double) → new_esEs14(zu311001, zu36001)
new_esEs28(zu31100, zu3600, ty_@0) → new_esEs12(zu31100, zu3600)
new_esEs22(zu311000, zu36000, app(app(ty_Either, eh), fa)) → new_esEs19(zu311000, zu36000, eh, fa)
new_esEs24(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Double) → new_esEs14(zu31100, zu3600)
new_esEs22(zu311000, zu36000, app(app(ty_@2, ef), eg)) → new_esEs18(zu311000, zu36000, ef, eg)
new_esEs27(zu311010, zu36010, ty_Double) → new_esEs14(zu311010, zu36010)
new_primEqNat0(Succ(zu3110000), Zero) → False
new_primEqNat0(Zero, Succ(zu360000)) → False
new_esEs21(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(app(ty_@2, bda), bdb), dg) → new_esEs18(zu311000, zu36000, bda, bdb)
new_esEs25(zu311001, zu36001, app(ty_Maybe, hh)) → new_esEs6(zu311001, zu36001, hh)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_@0) → new_esEs12(zu311000, zu36000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(zu311000, zu36000, ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs27(zu311010, zu36010, ty_Float) → new_esEs11(zu311010, zu36010)
new_esEs14(Double(zu311000, zu311001), Double(zu36000, zu36001)) → new_esEs9(new_sr(zu311000, zu36000), new_sr(zu311001, zu36001))
new_esEs26(zu311002, zu36002, app(app(app(ty_@3, bbc), bbd), bbe)) → new_esEs13(zu311002, zu36002, bbc, bbd, bbe)
new_esEs22(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs27(zu311010, zu36010, app(app(app(ty_@3, cg), da), db)) → new_esEs13(zu311010, zu36010, cg, da, db)
new_esEs7(False, False) → True
new_esEs27(zu311010, zu36010, ty_Integer) → new_esEs16(zu311010, zu36010)
new_esEs22(zu311000, zu36000, app(ty_[], ee)) → new_esEs17(zu311000, zu36000, ee)
new_esEs27(zu311010, zu36010, app(ty_Ratio, cf)) → new_esEs10(zu311010, zu36010, cf)
new_esEs24(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs25(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs25(zu311001, zu36001, ty_Bool) → new_esEs7(zu311001, zu36001)
new_esEs27(zu311010, zu36010, app(ty_[], dc)) → new_esEs17(zu311010, zu36010, dc)
new_esEs22(zu311000, zu36000, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, app(app(app(ty_@3, bdg), bdh), bea)) → new_esEs13(zu311000, zu36000, bdg, bdh, bea)
new_esEs27(zu311010, zu36010, ty_Int) → new_esEs9(zu311010, zu36010)
new_esEs22(zu311000, zu36000, ty_@0) → new_esEs12(zu311000, zu36000)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_[], ca)) → new_esEs17(zu311000, zu36000, ca)
new_esEs23(zu311001, zu36001, ty_Double) → new_esEs14(zu311001, zu36001)
new_esEs6(Just(zu311000), Just(zu36000), app(app(app(ty_@3, bf), bg), bh)) → new_esEs13(zu311000, zu36000, bf, bg, bh)
new_esEs16(Integer(zu311000), Integer(zu36000)) → new_primEqInt(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, app(ty_Ratio, bde)) → new_esEs10(zu311000, zu36000, bde)
new_esEs19(Right(zu311000), Right(zu36000), df, app(app(ty_Either, bee), bef)) → new_esEs19(zu311000, zu36000, bee, bef)
new_esEs25(zu311001, zu36001, ty_@0) → new_esEs12(zu311001, zu36001)
new_esEs26(zu311002, zu36002, ty_Bool) → new_esEs7(zu311002, zu36002)
new_esEs8(LT, LT) → True
new_sr(Neg(zu3110010), Neg(zu360010)) → Pos(new_primMulNat0(zu3110010, zu360010))
new_esEs25(zu311001, zu36001, ty_Ordering) → new_esEs8(zu311001, zu36001)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs25(zu311001, zu36001, app(app(ty_Either, bag), bah)) → new_esEs19(zu311001, zu36001, bag, bah)
new_esEs28(zu31100, zu3600, ty_Integer) → new_esEs16(zu31100, zu3600)
new_sr(Pos(zu3110010), Pos(zu360010)) → Pos(new_primMulNat0(zu3110010, zu360010))
new_asAs(False, zu66) → False
new_primEqNat0(Zero, Zero) → True
new_esEs6(Just(zu311000), Just(zu36000), ty_Char) → new_esEs15(zu311000, zu36000)
new_primMulNat0(Zero, Succ(zu3600100)) → Zero
new_primMulNat0(Succ(zu31100100), Zero) → Zero
new_esEs19(Right(zu311000), Left(zu36000), df, dg) → False
new_esEs19(Left(zu311000), Right(zu36000), df, dg) → False
new_esEs26(zu311002, zu36002, app(ty_Maybe, bbb)) → new_esEs6(zu311002, zu36002, bbb)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_Maybe, be)) → new_esEs6(zu311000, zu36000, be)
new_esEs23(zu311001, zu36001, app(app(ty_Either, gc), gd)) → new_esEs19(zu311001, zu36001, gc, gd)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(app(ty_Either, df), dg)) → new_esEs19(zu31100, zu3600, df, dg)
new_esEs19(Right(zu311000), Right(zu36000), df, app(app(ty_@2, bec), bed)) → new_esEs18(zu311000, zu36000, bec, bed)
new_esEs6(Just(zu311000), Just(zu36000), ty_@0) → new_esEs12(zu311000, zu36000)
new_esEs23(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_Ratio, bcc), dg) → new_esEs10(zu311000, zu36000, bcc)
new_esEs23(zu311001, zu36001, app(app(app(ty_@3, fd), ff), fg)) → new_esEs13(zu311001, zu36001, fd, ff, fg)
new_esEs17(:(zu311010, zu311011), :(zu36010, zu36011), bb) → new_asAs(new_esEs27(zu311010, zu36010, bb), new_esEs17(zu311011, zu36011, bb))
new_esEs6(Just(zu311000), Just(zu36000), ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs22(zu311000, zu36000, app(app(app(ty_@3, eb), ec), ed)) → new_esEs13(zu311000, zu36000, eb, ec, ed)
new_esEs24(zu311000, zu36000, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Bool) → new_esEs7(zu31100, zu3600)
new_esEs23(zu311001, zu36001, ty_Bool) → new_esEs7(zu311001, zu36001)
new_esEs23(zu311001, zu36001, app(ty_Maybe, fc)) → new_esEs6(zu311001, zu36001, fc)
new_esEs19(Right(zu311000), Right(zu36000), df, app(ty_[], beb)) → new_esEs17(zu311000, zu36000, beb)
new_esEs15(Char(zu311000), Char(zu36000)) → new_primEqNat0(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(app(ty_@2, dd), de)) → new_esEs18(zu31100, zu3600, dd, de)
new_esEs25(zu311001, zu36001, app(ty_[], bad)) → new_esEs17(zu311001, zu36001, bad)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Ordering) → new_esEs8(zu311002, zu36002)
new_esEs24(zu311000, zu36000, app(ty_Ratio, ge)) → new_esEs10(zu311000, zu36000, ge)
new_esEs8(GT, GT) → True
new_primPlusNat0(Succ(zu700), zu3600100) → Succ(Succ(new_primPlusNat1(zu700, zu3600100)))
new_esEs26(zu311002, zu36002, ty_Float) → new_esEs11(zu311002, zu36002)
new_esEs23(zu311001, zu36001, ty_@0) → new_esEs12(zu311001, zu36001)
new_esEs8(LT, GT) → False
new_esEs8(GT, LT) → False
new_esEs22(zu311000, zu36000, app(ty_Ratio, dh)) → new_esEs10(zu311000, zu36000, dh)
new_esEs19(Left(zu311000), Left(zu36000), ty_Double, dg) → new_esEs14(zu311000, zu36000)
new_esEs25(zu311001, zu36001, app(app(app(ty_@3, baa), bab), bac)) → new_esEs13(zu311001, zu36001, baa, bab, bac)
new_primEqInt(Neg(Succ(zu3110000)), Neg(Succ(zu360000))) → new_primEqNat0(zu3110000, zu360000)
new_esEs28(zu31100, zu3600, app(ty_[], dc)) → new_esEs17(zu31100, zu3600, dc)
new_esEs26(zu311002, zu36002, app(app(ty_Either, bca), bcb)) → new_esEs19(zu311002, zu36002, bca, bcb)
new_esEs23(zu311001, zu36001, ty_Ordering) → new_esEs8(zu311001, zu36001)
new_esEs25(zu311001, zu36001, app(app(ty_@2, bae), baf)) → new_esEs18(zu311001, zu36001, bae, baf)
new_esEs24(zu311000, zu36000, app(app(ty_@2, hc), hd)) → new_esEs18(zu311000, zu36000, hc, hd)
new_esEs28(zu31100, zu3600, ty_Char) → new_esEs15(zu31100, zu3600)
new_primPlusNat1(Zero, Succ(zu36001000)) → Succ(zu36001000)
new_primPlusNat1(Succ(zu7000), Zero) → Succ(zu7000)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_Ratio, bd)) → new_esEs10(zu311000, zu36000, bd)
new_esEs25(zu311001, zu36001, ty_Char) → new_esEs15(zu311001, zu36001)
new_esEs25(zu311001, zu36001, app(ty_Ratio, hg)) → new_esEs10(zu311001, zu36001, hg)
new_esEs7(True, True) → True
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs6(Just(zu311000), Just(zu36000), ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs22(zu311000, zu36000, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs24(zu311000, zu36000, app(app(app(ty_@3, gg), gh), ha)) → new_esEs13(zu311000, zu36000, gg, gh, ha)
new_esEs28(zu31100, zu3600, ty_Float) → new_esEs11(zu31100, zu3600)
new_esEs28(zu31100, zu3600, ty_Int) → new_esEs9(zu31100, zu3600)
new_esEs22(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_[], bch), dg) → new_esEs17(zu311000, zu36000, bch)
new_primEqInt(Neg(Zero), Neg(Succ(zu360000))) → False
new_primEqInt(Neg(Succ(zu3110000)), Neg(Zero)) → False
new_esEs6(Just(zu311000), Just(zu36000), app(app(ty_@2, cb), cc)) → new_esEs18(zu311000, zu36000, cb, cc)
new_esEs8(EQ, EQ) → True
new_esEs7(False, True) → False
new_esEs7(True, False) → False
new_esEs23(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), ty_Char, dg) → new_esEs15(zu311000, zu36000)
new_esEs20(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs19(Left(zu311000), Left(zu36000), app(app(app(ty_@3, bce), bcf), bcg), dg) → new_esEs13(zu311000, zu36000, bce, bcf, bcg)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs10(:%(zu311000, zu311001), :%(zu36000, zu36001), cf) → new_asAs(new_esEs20(zu311000, zu36000, cf), new_esEs21(zu311001, zu36001, cf))
new_asAs(True, zu66) → zu66
new_esEs27(zu311010, zu36010, ty_Bool) → new_esEs7(zu311010, zu36010)
new_esEs19(Left(zu311000), Left(zu36000), ty_Int, dg) → new_esEs9(zu311000, zu36000)
new_primMulNat0(Succ(zu31100100), Succ(zu3600100)) → new_primPlusNat0(new_primMulNat0(zu31100100, Succ(zu3600100)), zu3600100)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_Maybe, bcd), dg) → new_esEs6(zu311000, zu36000, bcd)
new_esEs27(zu311010, zu36010, app(app(ty_Either, df), dg)) → new_esEs19(zu311010, zu36010, df, dg)
new_esEs25(zu311001, zu36001, ty_Float) → new_esEs11(zu311001, zu36001)
new_esEs26(zu311002, zu36002, ty_Integer) → new_esEs16(zu311002, zu36002)
new_esEs6(Nothing, Nothing, bc) → True
new_esEs19(Left(zu311000), Left(zu36000), ty_Float, dg) → new_esEs11(zu311000, zu36000)
new_primEqInt(Pos(Succ(zu3110000)), Pos(Succ(zu360000))) → new_primEqNat0(zu3110000, zu360000)
new_esEs17([], [], bb) → True
new_esEs17([], :(zu36010, zu36011), bb) → False
new_esEs17(:(zu311010, zu311011), [], bb) → False
new_esEs25(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs11(Float(zu311000, zu311001), Float(zu36000, zu36001)) → new_esEs9(new_sr(zu311000, zu36000), new_sr(zu311001, zu36001))
new_esEs6(Just(zu311000), Nothing, bc) → False
new_esEs6(Nothing, Just(zu36000), bc) → False
new_primEqNat0(Succ(zu3110000), Succ(zu360000)) → new_primEqNat0(zu3110000, zu360000)
new_esEs27(zu311010, zu36010, ty_@0) → new_esEs12(zu311010, zu36010)
new_esEs27(zu311010, zu36010, ty_Ordering) → new_esEs8(zu311010, zu36010)
new_esEs9(zu31100, zu3600) → new_primEqInt(zu31100, zu3600)
new_esEs6(Just(zu311000), Just(zu36000), app(app(ty_Either, cd), ce)) → new_esEs19(zu311000, zu36000, cd, ce)
new_esEs19(Left(zu311000), Left(zu36000), ty_Integer, dg) → new_esEs16(zu311000, zu36000)
new_esEs24(zu311000, zu36000, app(ty_Maybe, gf)) → new_esEs6(zu311000, zu36000, gf)
new_esEs13(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), cg, da, db) → new_asAs(new_esEs24(zu311000, zu36000, cg), new_asAs(new_esEs25(zu311001, zu36001, da), new_esEs26(zu311002, zu36002, db)))
new_esEs26(zu311002, zu36002, ty_@0) → new_esEs12(zu311002, zu36002)
new_esEs24(zu311000, zu36000, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs22(zu311000, zu36000, ty_Char) → new_esEs15(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Ordering) → new_esEs8(zu31100, zu3600)
new_esEs6(Just(zu311000), Just(zu36000), ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs8(LT, EQ) → False
new_esEs8(EQ, LT) → False
new_primEqInt(Pos(Succ(zu3110000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(zu360000))) → False
new_esEs19(Left(zu311000), Left(zu36000), ty_Bool, dg) → new_esEs7(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_@0) → new_esEs12(zu311000, zu36000)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_Double) → new_esEs14(zu311000, zu36000)
The set Q consists of the following terms:
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs28(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_@0)
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs20(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_esEs7(False, False)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs8(EQ, EQ)
new_sr(Pos(x0), Pos(x1))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Char)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(:(x0, x1), [], x2)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Integer)
new_asAs(False, x0)
new_esEs26(x0, x1, ty_Bool)
new_esEs8(GT, GT)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Ordering)
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Double)
new_esEs8(LT, LT)
new_esEs7(True, False)
new_esEs7(False, True)
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs15(Char(x0), Char(x1))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs8(EQ, GT)
new_esEs8(GT, EQ)
new_esEs28(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_asAs(True, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs28(x0, x1, ty_Char)
new_esEs8(GT, LT)
new_esEs8(LT, GT)
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Nothing, x1)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs24(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_primEqNat0(Zero, Zero)
new_sr(Neg(x0), Neg(x1))
new_primPlusNat0(Succ(x0), x1)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs23(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Int)
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(@0, @0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs28(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(x0, x1)
new_esEs28(x0, x1, ty_Bool)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs6(Nothing, Nothing, x0)
new_esEs22(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs7(True, True)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs28(x0, x1, ty_Int)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs26(x0, x1, ty_Float)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs16(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, ty_Char)
new_esEs28(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_@0)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs8(LT, EQ)
new_esEs8(EQ, LT)
new_esEs23(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_esEs27(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs23(x0, x1, ty_Float)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs6(Just(x0), Just(x1), ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Float)
new_esEs28(x0, x1, ty_@0)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs28(x0, x1, ty_Float)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17([], :(x0, x1), x2)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs27(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Zero)
new_esEs17([], [], x0)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_deleteBy(:(zu31100, zu31101), :([], zu361), bb) → new_deleteBy(:(zu31100, zu31101), zu361, bb)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
- new_deleteBy(:(zu31100, zu31101), :(:(zu3600, zu3601), zu361), bb) → new_deleteBy0(zu361, zu3600, zu3601, zu31100, zu31101, new_asAs(new_esEs28(zu31100, zu3600, bb), new_esEs17(zu31101, zu3601, bb)), bb)
The graph contains the following edges 2 > 1, 2 > 2, 2 > 3, 1 > 4, 1 > 5, 3 >= 7
- new_deleteBy0(zu45, zu46, zu47, zu48, zu49, False, ba) → new_deleteBy(:(zu48, zu49), zu45, ba)
The graph contains the following edges 1 >= 2, 7 >= 3
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy([], :(:(zu3600, zu3601), zu361), bb) → new_deleteBy([], zu361, bb)
The TRS R consists of the following rules:
new_esEs19(Left(zu311000), Left(zu36000), ty_Ordering, dg) → new_esEs8(zu311000, zu36000)
new_primPlusNat1(Succ(zu7000), Succ(zu36001000)) → Succ(Succ(new_primPlusNat1(zu7000, zu36001000)))
new_esEs24(zu311000, zu36000, ty_Char) → new_esEs15(zu311000, zu36000)
new_primEqInt(Neg(Succ(zu3110000)), Pos(zu36000)) → False
new_primEqInt(Pos(Succ(zu3110000)), Neg(zu36000)) → False
new_esEs23(zu311001, zu36001, app(app(ty_@2, ga), gb)) → new_esEs18(zu311001, zu36001, ga, gb)
new_esEs6(Just(zu311000), Just(zu36000), ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Double) → new_esEs14(zu311002, zu36002)
new_esEs26(zu311002, zu36002, ty_Int) → new_esEs9(zu311002, zu36002)
new_esEs28(zu31100, zu3600, app(ty_Maybe, bc)) → new_esEs6(zu31100, zu3600, bc)
new_primEqInt(Neg(Zero), Pos(Succ(zu360000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(zu360000))) → False
new_esEs26(zu311002, zu36002, app(ty_[], bbf)) → new_esEs17(zu311002, zu36002, bbf)
new_esEs19(Right(zu311000), Right(zu36000), df, app(ty_Maybe, bdf)) → new_esEs6(zu311000, zu36000, bdf)
new_esEs23(zu311001, zu36001, app(ty_Ratio, fb)) → new_esEs10(zu311001, zu36001, fb)
new_esEs20(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs23(zu311001, zu36001, app(ty_[], fh)) → new_esEs17(zu311001, zu36001, fh)
new_esEs8(EQ, GT) → False
new_esEs8(GT, EQ) → False
new_esEs19(Left(zu311000), Left(zu36000), ty_@0, dg) → new_esEs12(zu311000, zu36000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs6(Just(zu311000), Just(zu36000), ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs26(zu311002, zu36002, app(ty_Ratio, bba)) → new_esEs10(zu311002, zu36002, bba)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Char) → new_esEs15(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(ty_Ratio, cf)) → new_esEs10(zu31100, zu3600, cf)
new_esEs23(zu311001, zu36001, ty_Float) → new_esEs11(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(app(ty_Either, bdc), bdd), dg) → new_esEs19(zu311000, zu36000, bdc, bdd)
new_primPlusNat0(Zero, zu3600100) → Succ(zu3600100)
new_esEs22(zu311000, zu36000, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(app(app(ty_@3, cg), da), db)) → new_esEs13(zu31100, zu3600, cg, da, db)
new_esEs6(Just(zu311000), Just(zu36000), ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Char) → new_esEs15(zu311002, zu36002)
new_sr(Neg(zu3110010), Pos(zu360010)) → Neg(new_primMulNat0(zu3110010, zu360010))
new_sr(Pos(zu3110010), Neg(zu360010)) → Neg(new_primMulNat0(zu3110010, zu360010))
new_esEs23(zu311001, zu36001, ty_Char) → new_esEs15(zu311001, zu36001)
new_esEs27(zu311010, zu36010, app(app(ty_@2, dd), de)) → new_esEs18(zu311010, zu36010, dd, de)
new_esEs24(zu311000, zu36000, app(ty_[], hb)) → new_esEs17(zu311000, zu36000, hb)
new_esEs24(zu311000, zu36000, app(app(ty_Either, he), hf)) → new_esEs19(zu311000, zu36000, he, hf)
new_esEs27(zu311010, zu36010, ty_Char) → new_esEs15(zu311010, zu36010)
new_esEs18(@2(zu311000, zu311001), @2(zu36000, zu36001), dd, de) → new_asAs(new_esEs22(zu311000, zu36000, dd), new_esEs23(zu311001, zu36001, de))
new_esEs21(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs22(zu311000, zu36000, app(ty_Maybe, ea)) → new_esEs6(zu311000, zu36000, ea)
new_esEs27(zu311010, zu36010, app(ty_Maybe, bc)) → new_esEs6(zu311010, zu36010, bc)
new_esEs26(zu311002, zu36002, app(app(ty_@2, bbg), bbh)) → new_esEs18(zu311002, zu36002, bbg, bbh)
new_esEs12(@0, @0) → True
new_esEs25(zu311001, zu36001, ty_Double) → new_esEs14(zu311001, zu36001)
new_esEs28(zu31100, zu3600, ty_@0) → new_esEs12(zu31100, zu3600)
new_esEs22(zu311000, zu36000, app(app(ty_Either, eh), fa)) → new_esEs19(zu311000, zu36000, eh, fa)
new_esEs24(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Double) → new_esEs14(zu31100, zu3600)
new_esEs22(zu311000, zu36000, app(app(ty_@2, ef), eg)) → new_esEs18(zu311000, zu36000, ef, eg)
new_esEs27(zu311010, zu36010, ty_Double) → new_esEs14(zu311010, zu36010)
new_primEqNat0(Succ(zu3110000), Zero) → False
new_primEqNat0(Zero, Succ(zu360000)) → False
new_esEs21(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(app(ty_@2, bda), bdb), dg) → new_esEs18(zu311000, zu36000, bda, bdb)
new_esEs25(zu311001, zu36001, app(ty_Maybe, hh)) → new_esEs6(zu311001, zu36001, hh)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_@0) → new_esEs12(zu311000, zu36000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(zu311000, zu36000, ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs27(zu311010, zu36010, ty_Float) → new_esEs11(zu311010, zu36010)
new_esEs14(Double(zu311000, zu311001), Double(zu36000, zu36001)) → new_esEs9(new_sr(zu311000, zu36000), new_sr(zu311001, zu36001))
new_esEs26(zu311002, zu36002, app(app(app(ty_@3, bbc), bbd), bbe)) → new_esEs13(zu311002, zu36002, bbc, bbd, bbe)
new_esEs22(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs27(zu311010, zu36010, app(app(app(ty_@3, cg), da), db)) → new_esEs13(zu311010, zu36010, cg, da, db)
new_esEs7(False, False) → True
new_esEs27(zu311010, zu36010, ty_Integer) → new_esEs16(zu311010, zu36010)
new_esEs22(zu311000, zu36000, app(ty_[], ee)) → new_esEs17(zu311000, zu36000, ee)
new_esEs27(zu311010, zu36010, app(ty_Ratio, cf)) → new_esEs10(zu311010, zu36010, cf)
new_esEs24(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs25(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs25(zu311001, zu36001, ty_Bool) → new_esEs7(zu311001, zu36001)
new_esEs27(zu311010, zu36010, app(ty_[], dc)) → new_esEs17(zu311010, zu36010, dc)
new_esEs22(zu311000, zu36000, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, app(app(app(ty_@3, bdg), bdh), bea)) → new_esEs13(zu311000, zu36000, bdg, bdh, bea)
new_esEs27(zu311010, zu36010, ty_Int) → new_esEs9(zu311010, zu36010)
new_esEs22(zu311000, zu36000, ty_@0) → new_esEs12(zu311000, zu36000)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_[], ca)) → new_esEs17(zu311000, zu36000, ca)
new_esEs23(zu311001, zu36001, ty_Double) → new_esEs14(zu311001, zu36001)
new_esEs6(Just(zu311000), Just(zu36000), app(app(app(ty_@3, bf), bg), bh)) → new_esEs13(zu311000, zu36000, bf, bg, bh)
new_esEs16(Integer(zu311000), Integer(zu36000)) → new_primEqInt(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, app(ty_Ratio, bde)) → new_esEs10(zu311000, zu36000, bde)
new_esEs19(Right(zu311000), Right(zu36000), df, app(app(ty_Either, bee), bef)) → new_esEs19(zu311000, zu36000, bee, bef)
new_esEs25(zu311001, zu36001, ty_@0) → new_esEs12(zu311001, zu36001)
new_esEs26(zu311002, zu36002, ty_Bool) → new_esEs7(zu311002, zu36002)
new_esEs8(LT, LT) → True
new_sr(Neg(zu3110010), Neg(zu360010)) → Pos(new_primMulNat0(zu3110010, zu360010))
new_esEs25(zu311001, zu36001, ty_Ordering) → new_esEs8(zu311001, zu36001)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs25(zu311001, zu36001, app(app(ty_Either, bag), bah)) → new_esEs19(zu311001, zu36001, bag, bah)
new_esEs28(zu31100, zu3600, ty_Integer) → new_esEs16(zu31100, zu3600)
new_sr(Pos(zu3110010), Pos(zu360010)) → Pos(new_primMulNat0(zu3110010, zu360010))
new_asAs(False, zu66) → False
new_primEqNat0(Zero, Zero) → True
new_esEs6(Just(zu311000), Just(zu36000), ty_Char) → new_esEs15(zu311000, zu36000)
new_primMulNat0(Zero, Succ(zu3600100)) → Zero
new_primMulNat0(Succ(zu31100100), Zero) → Zero
new_esEs19(Right(zu311000), Left(zu36000), df, dg) → False
new_esEs19(Left(zu311000), Right(zu36000), df, dg) → False
new_esEs26(zu311002, zu36002, app(ty_Maybe, bbb)) → new_esEs6(zu311002, zu36002, bbb)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_Maybe, be)) → new_esEs6(zu311000, zu36000, be)
new_esEs23(zu311001, zu36001, app(app(ty_Either, gc), gd)) → new_esEs19(zu311001, zu36001, gc, gd)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(app(ty_Either, df), dg)) → new_esEs19(zu31100, zu3600, df, dg)
new_esEs19(Right(zu311000), Right(zu36000), df, app(app(ty_@2, bec), bed)) → new_esEs18(zu311000, zu36000, bec, bed)
new_esEs6(Just(zu311000), Just(zu36000), ty_@0) → new_esEs12(zu311000, zu36000)
new_esEs23(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_Ratio, bcc), dg) → new_esEs10(zu311000, zu36000, bcc)
new_esEs23(zu311001, zu36001, app(app(app(ty_@3, fd), ff), fg)) → new_esEs13(zu311001, zu36001, fd, ff, fg)
new_esEs17(:(zu311010, zu311011), :(zu36010, zu36011), bb) → new_asAs(new_esEs27(zu311010, zu36010, bb), new_esEs17(zu311011, zu36011, bb))
new_esEs6(Just(zu311000), Just(zu36000), ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs22(zu311000, zu36000, app(app(app(ty_@3, eb), ec), ed)) → new_esEs13(zu311000, zu36000, eb, ec, ed)
new_esEs24(zu311000, zu36000, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Bool) → new_esEs7(zu31100, zu3600)
new_esEs23(zu311001, zu36001, ty_Bool) → new_esEs7(zu311001, zu36001)
new_esEs23(zu311001, zu36001, app(ty_Maybe, fc)) → new_esEs6(zu311001, zu36001, fc)
new_esEs19(Right(zu311000), Right(zu36000), df, app(ty_[], beb)) → new_esEs17(zu311000, zu36000, beb)
new_esEs15(Char(zu311000), Char(zu36000)) → new_primEqNat0(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(app(ty_@2, dd), de)) → new_esEs18(zu31100, zu3600, dd, de)
new_esEs25(zu311001, zu36001, app(ty_[], bad)) → new_esEs17(zu311001, zu36001, bad)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Ordering) → new_esEs8(zu311002, zu36002)
new_esEs24(zu311000, zu36000, app(ty_Ratio, ge)) → new_esEs10(zu311000, zu36000, ge)
new_esEs8(GT, GT) → True
new_primPlusNat0(Succ(zu700), zu3600100) → Succ(Succ(new_primPlusNat1(zu700, zu3600100)))
new_esEs26(zu311002, zu36002, ty_Float) → new_esEs11(zu311002, zu36002)
new_esEs23(zu311001, zu36001, ty_@0) → new_esEs12(zu311001, zu36001)
new_esEs8(LT, GT) → False
new_esEs8(GT, LT) → False
new_esEs22(zu311000, zu36000, app(ty_Ratio, dh)) → new_esEs10(zu311000, zu36000, dh)
new_esEs19(Left(zu311000), Left(zu36000), ty_Double, dg) → new_esEs14(zu311000, zu36000)
new_esEs25(zu311001, zu36001, app(app(app(ty_@3, baa), bab), bac)) → new_esEs13(zu311001, zu36001, baa, bab, bac)
new_primEqInt(Neg(Succ(zu3110000)), Neg(Succ(zu360000))) → new_primEqNat0(zu3110000, zu360000)
new_esEs28(zu31100, zu3600, app(ty_[], dc)) → new_esEs17(zu31100, zu3600, dc)
new_esEs26(zu311002, zu36002, app(app(ty_Either, bca), bcb)) → new_esEs19(zu311002, zu36002, bca, bcb)
new_esEs23(zu311001, zu36001, ty_Ordering) → new_esEs8(zu311001, zu36001)
new_esEs25(zu311001, zu36001, app(app(ty_@2, bae), baf)) → new_esEs18(zu311001, zu36001, bae, baf)
new_esEs24(zu311000, zu36000, app(app(ty_@2, hc), hd)) → new_esEs18(zu311000, zu36000, hc, hd)
new_esEs28(zu31100, zu3600, ty_Char) → new_esEs15(zu31100, zu3600)
new_primPlusNat1(Zero, Succ(zu36001000)) → Succ(zu36001000)
new_primPlusNat1(Succ(zu7000), Zero) → Succ(zu7000)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_Ratio, bd)) → new_esEs10(zu311000, zu36000, bd)
new_esEs25(zu311001, zu36001, ty_Char) → new_esEs15(zu311001, zu36001)
new_esEs25(zu311001, zu36001, app(ty_Ratio, hg)) → new_esEs10(zu311001, zu36001, hg)
new_esEs7(True, True) → True
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs6(Just(zu311000), Just(zu36000), ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs22(zu311000, zu36000, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs24(zu311000, zu36000, app(app(app(ty_@3, gg), gh), ha)) → new_esEs13(zu311000, zu36000, gg, gh, ha)
new_esEs28(zu31100, zu3600, ty_Float) → new_esEs11(zu31100, zu3600)
new_esEs28(zu31100, zu3600, ty_Int) → new_esEs9(zu31100, zu3600)
new_esEs22(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_[], bch), dg) → new_esEs17(zu311000, zu36000, bch)
new_primEqInt(Neg(Zero), Neg(Succ(zu360000))) → False
new_primEqInt(Neg(Succ(zu3110000)), Neg(Zero)) → False
new_esEs6(Just(zu311000), Just(zu36000), app(app(ty_@2, cb), cc)) → new_esEs18(zu311000, zu36000, cb, cc)
new_esEs8(EQ, EQ) → True
new_esEs7(False, True) → False
new_esEs7(True, False) → False
new_esEs23(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), ty_Char, dg) → new_esEs15(zu311000, zu36000)
new_esEs20(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs19(Left(zu311000), Left(zu36000), app(app(app(ty_@3, bce), bcf), bcg), dg) → new_esEs13(zu311000, zu36000, bce, bcf, bcg)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs10(:%(zu311000, zu311001), :%(zu36000, zu36001), cf) → new_asAs(new_esEs20(zu311000, zu36000, cf), new_esEs21(zu311001, zu36001, cf))
new_asAs(True, zu66) → zu66
new_esEs27(zu311010, zu36010, ty_Bool) → new_esEs7(zu311010, zu36010)
new_esEs19(Left(zu311000), Left(zu36000), ty_Int, dg) → new_esEs9(zu311000, zu36000)
new_primMulNat0(Succ(zu31100100), Succ(zu3600100)) → new_primPlusNat0(new_primMulNat0(zu31100100, Succ(zu3600100)), zu3600100)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_Maybe, bcd), dg) → new_esEs6(zu311000, zu36000, bcd)
new_esEs27(zu311010, zu36010, app(app(ty_Either, df), dg)) → new_esEs19(zu311010, zu36010, df, dg)
new_esEs25(zu311001, zu36001, ty_Float) → new_esEs11(zu311001, zu36001)
new_esEs26(zu311002, zu36002, ty_Integer) → new_esEs16(zu311002, zu36002)
new_esEs6(Nothing, Nothing, bc) → True
new_esEs19(Left(zu311000), Left(zu36000), ty_Float, dg) → new_esEs11(zu311000, zu36000)
new_primEqInt(Pos(Succ(zu3110000)), Pos(Succ(zu360000))) → new_primEqNat0(zu3110000, zu360000)
new_esEs17([], [], bb) → True
new_esEs17([], :(zu36010, zu36011), bb) → False
new_esEs17(:(zu311010, zu311011), [], bb) → False
new_esEs25(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs11(Float(zu311000, zu311001), Float(zu36000, zu36001)) → new_esEs9(new_sr(zu311000, zu36000), new_sr(zu311001, zu36001))
new_esEs6(Just(zu311000), Nothing, bc) → False
new_esEs6(Nothing, Just(zu36000), bc) → False
new_primEqNat0(Succ(zu3110000), Succ(zu360000)) → new_primEqNat0(zu3110000, zu360000)
new_esEs27(zu311010, zu36010, ty_@0) → new_esEs12(zu311010, zu36010)
new_esEs27(zu311010, zu36010, ty_Ordering) → new_esEs8(zu311010, zu36010)
new_esEs9(zu31100, zu3600) → new_primEqInt(zu31100, zu3600)
new_esEs6(Just(zu311000), Just(zu36000), app(app(ty_Either, cd), ce)) → new_esEs19(zu311000, zu36000, cd, ce)
new_esEs19(Left(zu311000), Left(zu36000), ty_Integer, dg) → new_esEs16(zu311000, zu36000)
new_esEs24(zu311000, zu36000, app(ty_Maybe, gf)) → new_esEs6(zu311000, zu36000, gf)
new_esEs13(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), cg, da, db) → new_asAs(new_esEs24(zu311000, zu36000, cg), new_asAs(new_esEs25(zu311001, zu36001, da), new_esEs26(zu311002, zu36002, db)))
new_esEs26(zu311002, zu36002, ty_@0) → new_esEs12(zu311002, zu36002)
new_esEs24(zu311000, zu36000, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs22(zu311000, zu36000, ty_Char) → new_esEs15(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Ordering) → new_esEs8(zu31100, zu3600)
new_esEs6(Just(zu311000), Just(zu36000), ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs8(LT, EQ) → False
new_esEs8(EQ, LT) → False
new_primEqInt(Pos(Succ(zu3110000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(zu360000))) → False
new_esEs19(Left(zu311000), Left(zu36000), ty_Bool, dg) → new_esEs7(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_@0) → new_esEs12(zu311000, zu36000)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs19(Right(zu311000), Right(zu36000), df, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_Double) → new_esEs14(zu311000, zu36000)
The set Q consists of the following terms:
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs28(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_@0)
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs20(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_esEs7(False, False)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs8(EQ, EQ)
new_sr(Pos(x0), Pos(x1))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Char)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(:(x0, x1), [], x2)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Integer)
new_asAs(False, x0)
new_esEs26(x0, x1, ty_Bool)
new_esEs8(GT, GT)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Ordering)
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Double)
new_esEs8(LT, LT)
new_esEs7(True, False)
new_esEs7(False, True)
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs15(Char(x0), Char(x1))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs8(EQ, GT)
new_esEs8(GT, EQ)
new_esEs28(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_asAs(True, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs28(x0, x1, ty_Char)
new_esEs8(GT, LT)
new_esEs8(LT, GT)
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Nothing, x1)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs24(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_primEqNat0(Zero, Zero)
new_sr(Neg(x0), Neg(x1))
new_primPlusNat0(Succ(x0), x1)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs23(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Int)
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(@0, @0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs28(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(x0, x1)
new_esEs28(x0, x1, ty_Bool)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs6(Nothing, Nothing, x0)
new_esEs22(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs7(True, True)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs28(x0, x1, ty_Int)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs26(x0, x1, ty_Float)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs16(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, ty_Char)
new_esEs28(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_@0)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs8(LT, EQ)
new_esEs8(EQ, LT)
new_esEs23(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_esEs27(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs23(x0, x1, ty_Float)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs6(Just(x0), Just(x1), ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Float)
new_esEs28(x0, x1, ty_@0)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs28(x0, x1, ty_Float)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17([], :(x0, x1), x2)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs27(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Zero)
new_esEs17([], [], x0)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy([], :(:(zu3600, zu3601), zu361), bb) → new_deleteBy([], zu361, bb)
R is empty.
The set Q consists of the following terms:
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs28(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_@0)
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs20(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_esEs7(False, False)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs8(EQ, EQ)
new_sr(Pos(x0), Pos(x1))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Char)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(:(x0, x1), [], x2)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Integer)
new_asAs(False, x0)
new_esEs26(x0, x1, ty_Bool)
new_esEs8(GT, GT)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Ordering)
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Double)
new_esEs8(LT, LT)
new_esEs7(True, False)
new_esEs7(False, True)
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs15(Char(x0), Char(x1))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs8(EQ, GT)
new_esEs8(GT, EQ)
new_esEs28(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_asAs(True, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs28(x0, x1, ty_Char)
new_esEs8(GT, LT)
new_esEs8(LT, GT)
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Nothing, x1)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs24(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_primEqNat0(Zero, Zero)
new_sr(Neg(x0), Neg(x1))
new_primPlusNat0(Succ(x0), x1)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs23(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Int)
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(@0, @0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs28(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(x0, x1)
new_esEs28(x0, x1, ty_Bool)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs6(Nothing, Nothing, x0)
new_esEs22(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs7(True, True)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs28(x0, x1, ty_Int)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs26(x0, x1, ty_Float)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs16(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, ty_Char)
new_esEs28(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_@0)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs8(LT, EQ)
new_esEs8(EQ, LT)
new_esEs23(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_esEs27(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs23(x0, x1, ty_Float)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs6(Just(x0), Just(x1), ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Float)
new_esEs28(x0, x1, ty_@0)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs28(x0, x1, ty_Float)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17([], :(x0, x1), x2)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs27(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Zero)
new_esEs17([], [], x0)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs28(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_@0)
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs20(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_esEs7(False, False)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs8(EQ, EQ)
new_sr(Pos(x0), Pos(x1))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Char)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(:(x0, x1), [], x2)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Integer)
new_asAs(False, x0)
new_esEs26(x0, x1, ty_Bool)
new_esEs8(GT, GT)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Ordering)
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Double)
new_esEs8(LT, LT)
new_esEs7(True, False)
new_esEs7(False, True)
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs15(Char(x0), Char(x1))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs8(EQ, GT)
new_esEs8(GT, EQ)
new_esEs28(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_asAs(True, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs28(x0, x1, ty_Char)
new_esEs8(GT, LT)
new_esEs8(LT, GT)
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Nothing, x1)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs24(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_primEqNat0(Zero, Zero)
new_sr(Neg(x0), Neg(x1))
new_primPlusNat0(Succ(x0), x1)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs23(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Int)
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(@0, @0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs28(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(x0, x1)
new_esEs28(x0, x1, ty_Bool)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs6(Nothing, Nothing, x0)
new_esEs22(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Zero)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs7(True, True)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs28(x0, x1, ty_Int)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs26(x0, x1, ty_Float)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs16(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, ty_Char)
new_esEs28(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_@0)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs8(LT, EQ)
new_esEs8(EQ, LT)
new_esEs23(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_esEs27(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs23(x0, x1, ty_Float)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs6(Just(x0), Just(x1), ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Float)
new_esEs28(x0, x1, ty_@0)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs28(x0, x1, ty_Float)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17([], :(x0, x1), x2)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs27(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Zero)
new_esEs17([], [], x0)
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy([], :(:(zu3600, zu3601), zu361), bb) → new_deleteBy([], zu361, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_deleteBy([], :(:(zu3600, zu3601), zu361), bb) → new_deleteBy([], zu361, bb)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldl(zu36, :(zu3110, zu3111), ba) → new_foldl(new_deleteBy1(zu3110, zu36, ba), zu3111, ba)
The TRS R consists of the following rules:
new_esEs19(Left(zu311000), Left(zu36000), ty_Ordering, bbh) → new_esEs8(zu311000, zu36000)
new_primPlusNat1(Succ(zu7000), Succ(zu36001000)) → Succ(Succ(new_primPlusNat1(zu7000, zu36001000)))
new_primEqInt(Neg(Succ(zu3110000)), Pos(zu36000)) → False
new_primEqInt(Pos(Succ(zu3110000)), Neg(zu36000)) → False
new_esEs24(zu311000, zu36000, ty_Char) → new_esEs15(zu311000, zu36000)
new_esEs23(zu311001, zu36001, app(app(ty_@2, fb), fc)) → new_esEs18(zu311001, zu36001, fb, fc)
new_esEs6(Just(zu311000), Just(zu36000), ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(ty_Maybe, bb)) → new_esEs6(zu31100, zu3600, bb)
new_esEs26(zu311002, zu36002, ty_Double) → new_esEs14(zu311002, zu36002)
new_esEs26(zu311002, zu36002, ty_Int) → new_esEs9(zu311002, zu36002)
new_primEqInt(Neg(Zero), Pos(Succ(zu360000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(zu360000))) → False
new_esEs26(zu311002, zu36002, app(ty_[], bbc)) → new_esEs17(zu311002, zu36002, bbc)
new_esEs19(Right(zu311000), Right(zu36000), bdc, app(ty_Maybe, bde)) → new_esEs6(zu311000, zu36000, bde)
new_esEs23(zu311001, zu36001, app(ty_Ratio, ed)) → new_esEs10(zu311001, zu36001, ed)
new_esEs20(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs23(zu311001, zu36001, app(ty_[], fa)) → new_esEs17(zu311001, zu36001, fa)
new_esEs8(EQ, GT) → False
new_esEs8(GT, EQ) → False
new_esEs19(Left(zu311000), Left(zu36000), ty_@0, bbh) → new_esEs12(zu311000, zu36000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs6(Just(zu311000), Just(zu36000), ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), bdc, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_deleteBy1(:(zu31100, zu31101), :(:(zu3600, zu3601), zu361), ba) → new_deleteBy00(zu361, zu3600, zu3601, zu31100, zu31101, new_asAs(new_esEs28(zu31100, zu3600, ba), new_esEs17(zu31101, zu3601, ba)), ba)
new_esEs26(zu311002, zu36002, app(ty_Ratio, baf)) → new_esEs10(zu311002, zu36002, baf)
new_esEs19(Right(zu311000), Right(zu36000), bdc, ty_Char) → new_esEs15(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(ty_Ratio, cf)) → new_esEs10(zu31100, zu3600, cf)
new_esEs23(zu311001, zu36001, ty_Float) → new_esEs11(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(app(ty_Either, bda), bdb), bbh) → new_esEs19(zu311000, zu36000, bda, bdb)
new_primPlusNat0(Zero, zu3600100) → Succ(zu3600100)
new_esEs22(zu311000, zu36000, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(app(app(ty_@3, fg), fh), ga)) → new_esEs13(zu31100, zu3600, fg, fh, ga)
new_esEs6(Just(zu311000), Just(zu36000), ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Char) → new_esEs15(zu311002, zu36002)
new_sr(Neg(zu3110010), Pos(zu360010)) → Neg(new_primMulNat0(zu3110010, zu360010))
new_sr(Pos(zu3110010), Neg(zu360010)) → Neg(new_primMulNat0(zu3110010, zu360010))
new_esEs23(zu311001, zu36001, ty_Char) → new_esEs15(zu311001, zu36001)
new_esEs27(zu311010, zu36010, app(app(ty_@2, cg), da)) → new_esEs18(zu311010, zu36010, cg, da)
new_esEs24(zu311000, zu36000, app(ty_[], gg)) → new_esEs17(zu311000, zu36000, gg)
new_esEs24(zu311000, zu36000, app(app(ty_Either, hb), hc)) → new_esEs19(zu311000, zu36000, hb, hc)
new_esEs27(zu311010, zu36010, ty_Char) → new_esEs15(zu311010, zu36010)
new_esEs18(@2(zu311000, zu311001), @2(zu36000, zu36001), cg, da) → new_asAs(new_esEs22(zu311000, zu36000, cg), new_esEs23(zu311001, zu36001, da))
new_esEs21(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs22(zu311000, zu36000, app(ty_Maybe, dc)) → new_esEs6(zu311000, zu36000, dc)
new_esEs27(zu311010, zu36010, app(ty_Maybe, bb)) → new_esEs6(zu311010, zu36010, bb)
new_esEs26(zu311002, zu36002, app(app(ty_@2, bbd), bbe)) → new_esEs18(zu311002, zu36002, bbd, bbe)
new_esEs12(@0, @0) → True
new_esEs25(zu311001, zu36001, ty_Double) → new_esEs14(zu311001, zu36001)
new_esEs28(zu31100, zu3600, ty_@0) → new_esEs12(zu31100, zu3600)
new_esEs22(zu311000, zu36000, app(app(ty_Either, eb), ec)) → new_esEs19(zu311000, zu36000, eb, ec)
new_esEs24(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Double) → new_esEs14(zu31100, zu3600)
new_esEs22(zu311000, zu36000, app(app(ty_@2, dh), ea)) → new_esEs18(zu311000, zu36000, dh, ea)
new_esEs27(zu311010, zu36010, ty_Double) → new_esEs14(zu311010, zu36010)
new_primEqNat0(Zero, Succ(zu360000)) → False
new_primEqNat0(Succ(zu3110000), Zero) → False
new_esEs21(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(app(ty_@2, bcg), bch), bbh) → new_esEs18(zu311000, zu36000, bcg, bch)
new_esEs25(zu311001, zu36001, app(ty_Maybe, he)) → new_esEs6(zu311001, zu36001, he)
new_esEs19(Right(zu311000), Right(zu36000), bdc, ty_@0) → new_esEs12(zu311000, zu36000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(zu311000, zu36000, ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs27(zu311010, zu36010, ty_Float) → new_esEs11(zu311010, zu36010)
new_esEs14(Double(zu311000, zu311001), Double(zu36000, zu36001)) → new_esEs9(new_sr(zu311000, zu36000), new_sr(zu311001, zu36001))
new_esEs26(zu311002, zu36002, app(app(app(ty_@3, bah), bba), bbb)) → new_esEs13(zu311002, zu36002, bah, bba, bbb)
new_esEs22(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs27(zu311010, zu36010, app(app(app(ty_@3, fg), fh), ga)) → new_esEs13(zu311010, zu36010, fg, fh, ga)
new_esEs7(False, False) → True
new_esEs27(zu311010, zu36010, ty_Integer) → new_esEs16(zu311010, zu36010)
new_esEs22(zu311000, zu36000, app(ty_[], dg)) → new_esEs17(zu311000, zu36000, dg)
new_deleteBy1([], :([], zu361), ba) → zu361
new_esEs24(zu311000, zu36000, ty_Int) → new_esEs9(zu311000, zu36000)
new_esEs27(zu311010, zu36010, app(ty_Ratio, cf)) → new_esEs10(zu311010, zu36010, cf)
new_esEs25(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs25(zu311001, zu36001, ty_Bool) → new_esEs7(zu311001, zu36001)
new_esEs27(zu311010, zu36010, app(ty_[], bef)) → new_esEs17(zu311010, zu36010, bef)
new_esEs22(zu311000, zu36000, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), bdc, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs13(zu311000, zu36000, bdf, bdg, bdh)
new_esEs27(zu311010, zu36010, ty_Int) → new_esEs9(zu311010, zu36010)
new_esEs22(zu311000, zu36000, ty_@0) → new_esEs12(zu311000, zu36000)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_[], bh)) → new_esEs17(zu311000, zu36000, bh)
new_esEs23(zu311001, zu36001, ty_Double) → new_esEs14(zu311001, zu36001)
new_esEs6(Just(zu311000), Just(zu36000), app(app(app(ty_@3, be), bf), bg)) → new_esEs13(zu311000, zu36000, be, bf, bg)
new_esEs16(Integer(zu311000), Integer(zu36000)) → new_primEqInt(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), bdc, app(ty_Ratio, bdd)) → new_esEs10(zu311000, zu36000, bdd)
new_esEs19(Right(zu311000), Right(zu36000), bdc, app(app(ty_Either, bed), bee)) → new_esEs19(zu311000, zu36000, bed, bee)
new_esEs25(zu311001, zu36001, ty_@0) → new_esEs12(zu311001, zu36001)
new_esEs26(zu311002, zu36002, ty_Bool) → new_esEs7(zu311002, zu36002)
new_esEs8(LT, LT) → True
new_sr(Neg(zu3110010), Neg(zu360010)) → Pos(new_primMulNat0(zu3110010, zu360010))
new_esEs25(zu311001, zu36001, ty_Ordering) → new_esEs8(zu311001, zu36001)
new_esEs19(Right(zu311000), Right(zu36000), bdc, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs25(zu311001, zu36001, app(app(ty_Either, bad), bae)) → new_esEs19(zu311001, zu36001, bad, bae)
new_deleteBy00(zu45, zu46, zu47, zu48, zu49, True, ce) → zu45
new_esEs28(zu31100, zu3600, ty_Integer) → new_esEs16(zu31100, zu3600)
new_sr(Pos(zu3110010), Pos(zu360010)) → Pos(new_primMulNat0(zu3110010, zu360010))
new_asAs(False, zu66) → False
new_primEqNat0(Zero, Zero) → True
new_esEs6(Just(zu311000), Just(zu36000), ty_Char) → new_esEs15(zu311000, zu36000)
new_primMulNat0(Zero, Succ(zu3600100)) → Zero
new_primMulNat0(Succ(zu31100100), Zero) → Zero
new_esEs19(Right(zu311000), Left(zu36000), bdc, bbh) → False
new_esEs19(Left(zu311000), Right(zu36000), bdc, bbh) → False
new_esEs26(zu311002, zu36002, app(ty_Maybe, bag)) → new_esEs6(zu311002, zu36002, bag)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_Maybe, bd)) → new_esEs6(zu311000, zu36000, bd)
new_esEs23(zu311001, zu36001, app(app(ty_Either, fd), ff)) → new_esEs19(zu311001, zu36001, fd, ff)
new_esEs19(Right(zu311000), Right(zu36000), bdc, ty_Int) → new_esEs9(zu311000, zu36000)
new_deleteBy00(zu45, zu46, zu47, zu48, zu49, False, ce) → :(:(zu46, zu47), new_deleteBy1(:(zu48, zu49), zu45, ce))
new_esEs28(zu31100, zu3600, app(app(ty_Either, bdc), bbh)) → new_esEs19(zu31100, zu3600, bdc, bbh)
new_esEs19(Right(zu311000), Right(zu36000), bdc, app(app(ty_@2, beb), bec)) → new_esEs18(zu311000, zu36000, beb, bec)
new_esEs6(Just(zu311000), Just(zu36000), ty_@0) → new_esEs12(zu311000, zu36000)
new_esEs23(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_Ratio, bca), bbh) → new_esEs10(zu311000, zu36000, bca)
new_esEs23(zu311001, zu36001, app(app(app(ty_@3, ef), eg), eh)) → new_esEs13(zu311001, zu36001, ef, eg, eh)
new_esEs17(:(zu311010, zu311011), :(zu36010, zu36011), ba) → new_asAs(new_esEs27(zu311010, zu36010, ba), new_esEs17(zu311011, zu36011, ba))
new_esEs6(Just(zu311000), Just(zu36000), ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs22(zu311000, zu36000, app(app(app(ty_@3, dd), de), df)) → new_esEs13(zu311000, zu36000, dd, de, df)
new_esEs24(zu311000, zu36000, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Bool) → new_esEs7(zu31100, zu3600)
new_esEs23(zu311001, zu36001, ty_Bool) → new_esEs7(zu311001, zu36001)
new_esEs23(zu311001, zu36001, app(ty_Maybe, ee)) → new_esEs6(zu311001, zu36001, ee)
new_esEs19(Right(zu311000), Right(zu36000), bdc, app(ty_[], bea)) → new_esEs17(zu311000, zu36000, bea)
new_esEs15(Char(zu311000), Char(zu36000)) → new_primEqNat0(zu311000, zu36000)
new_esEs28(zu31100, zu3600, app(app(ty_@2, cg), da)) → new_esEs18(zu31100, zu3600, cg, da)
new_esEs25(zu311001, zu36001, app(ty_[], baa)) → new_esEs17(zu311001, zu36001, baa)
new_esEs19(Right(zu311000), Right(zu36000), bdc, ty_Float) → new_esEs11(zu311000, zu36000)
new_esEs26(zu311002, zu36002, ty_Ordering) → new_esEs8(zu311002, zu36002)
new_deleteBy1(:(zu31100, zu31101), :([], zu361), ba) → :([], new_deleteBy1(:(zu31100, zu31101), zu361, ba))
new_esEs24(zu311000, zu36000, app(ty_Ratio, gb)) → new_esEs10(zu311000, zu36000, gb)
new_esEs8(GT, GT) → True
new_primPlusNat0(Succ(zu700), zu3600100) → Succ(Succ(new_primPlusNat1(zu700, zu3600100)))
new_esEs26(zu311002, zu36002, ty_Float) → new_esEs11(zu311002, zu36002)
new_esEs23(zu311001, zu36001, ty_@0) → new_esEs12(zu311001, zu36001)
new_esEs8(LT, GT) → False
new_esEs8(GT, LT) → False
new_esEs22(zu311000, zu36000, app(ty_Ratio, db)) → new_esEs10(zu311000, zu36000, db)
new_esEs19(Left(zu311000), Left(zu36000), ty_Double, bbh) → new_esEs14(zu311000, zu36000)
new_esEs25(zu311001, zu36001, app(app(app(ty_@3, hf), hg), hh)) → new_esEs13(zu311001, zu36001, hf, hg, hh)
new_primEqInt(Neg(Succ(zu3110000)), Neg(Succ(zu360000))) → new_primEqNat0(zu3110000, zu360000)
new_esEs28(zu31100, zu3600, app(ty_[], bef)) → new_esEs17(zu31100, zu3600, bef)
new_esEs26(zu311002, zu36002, app(app(ty_Either, bbf), bbg)) → new_esEs19(zu311002, zu36002, bbf, bbg)
new_esEs23(zu311001, zu36001, ty_Ordering) → new_esEs8(zu311001, zu36001)
new_esEs25(zu311001, zu36001, app(app(ty_@2, bab), bac)) → new_esEs18(zu311001, zu36001, bab, bac)
new_esEs24(zu311000, zu36000, app(app(ty_@2, gh), ha)) → new_esEs18(zu311000, zu36000, gh, ha)
new_esEs28(zu31100, zu3600, ty_Char) → new_esEs15(zu31100, zu3600)
new_primPlusNat1(Zero, Succ(zu36001000)) → Succ(zu36001000)
new_primPlusNat1(Succ(zu7000), Zero) → Succ(zu7000)
new_esEs6(Just(zu311000), Just(zu36000), app(ty_Ratio, bc)) → new_esEs10(zu311000, zu36000, bc)
new_esEs25(zu311001, zu36001, ty_Char) → new_esEs15(zu311001, zu36001)
new_esEs25(zu311001, zu36001, app(ty_Ratio, hd)) → new_esEs10(zu311001, zu36001, hd)
new_esEs7(True, True) → True
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs6(Just(zu311000), Just(zu36000), ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs22(zu311000, zu36000, ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs24(zu311000, zu36000, app(app(app(ty_@3, gd), ge), gf)) → new_esEs13(zu311000, zu36000, gd, ge, gf)
new_esEs28(zu31100, zu3600, ty_Float) → new_esEs11(zu31100, zu3600)
new_esEs28(zu31100, zu3600, ty_Int) → new_esEs9(zu31100, zu3600)
new_esEs22(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_[], bcf), bbh) → new_esEs17(zu311000, zu36000, bcf)
new_primEqInt(Neg(Zero), Neg(Succ(zu360000))) → False
new_primEqInt(Neg(Succ(zu3110000)), Neg(Zero)) → False
new_esEs6(Just(zu311000), Just(zu36000), app(app(ty_@2, ca), cb)) → new_esEs18(zu311000, zu36000, ca, cb)
new_esEs8(EQ, EQ) → True
new_esEs7(True, False) → False
new_esEs7(False, True) → False
new_esEs23(zu311001, zu36001, ty_Integer) → new_esEs16(zu311001, zu36001)
new_esEs19(Left(zu311000), Left(zu36000), ty_Char, bbh) → new_esEs15(zu311000, zu36000)
new_esEs20(zu311000, zu36000, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs19(Left(zu311000), Left(zu36000), app(app(app(ty_@3, bcc), bcd), bce), bbh) → new_esEs13(zu311000, zu36000, bcc, bcd, bce)
new_deleteBy1(zu3110, [], ba) → []
new_primPlusNat1(Zero, Zero) → Zero
new_esEs10(:%(zu311000, zu311001), :%(zu36000, zu36001), cf) → new_asAs(new_esEs20(zu311000, zu36000, cf), new_esEs21(zu311001, zu36001, cf))
new_asAs(True, zu66) → zu66
new_esEs27(zu311010, zu36010, ty_Bool) → new_esEs7(zu311010, zu36010)
new_esEs19(Left(zu311000), Left(zu36000), ty_Int, bbh) → new_esEs9(zu311000, zu36000)
new_primMulNat0(Succ(zu31100100), Succ(zu3600100)) → new_primPlusNat0(new_primMulNat0(zu31100100, Succ(zu3600100)), zu3600100)
new_esEs19(Left(zu311000), Left(zu36000), app(ty_Maybe, bcb), bbh) → new_esEs6(zu311000, zu36000, bcb)
new_esEs27(zu311010, zu36010, app(app(ty_Either, bdc), bbh)) → new_esEs19(zu311010, zu36010, bdc, bbh)
new_esEs25(zu311001, zu36001, ty_Float) → new_esEs11(zu311001, zu36001)
new_esEs26(zu311002, zu36002, ty_Integer) → new_esEs16(zu311002, zu36002)
new_esEs6(Nothing, Nothing, bb) → True
new_esEs19(Left(zu311000), Left(zu36000), ty_Float, bbh) → new_esEs11(zu311000, zu36000)
new_primEqInt(Pos(Succ(zu3110000)), Pos(Succ(zu360000))) → new_primEqNat0(zu3110000, zu360000)
new_esEs17([], [], ba) → True
new_esEs17([], :(zu36010, zu36011), ba) → False
new_esEs17(:(zu311010, zu311011), [], ba) → False
new_esEs25(zu311001, zu36001, ty_Int) → new_esEs9(zu311001, zu36001)
new_esEs11(Float(zu311000, zu311001), Float(zu36000, zu36001)) → new_esEs9(new_sr(zu311000, zu36000), new_sr(zu311001, zu36001))
new_esEs6(Just(zu311000), Nothing, bb) → False
new_esEs6(Nothing, Just(zu36000), bb) → False
new_primEqNat0(Succ(zu3110000), Succ(zu360000)) → new_primEqNat0(zu3110000, zu360000)
new_esEs27(zu311010, zu36010, ty_Ordering) → new_esEs8(zu311010, zu36010)
new_esEs9(zu31100, zu3600) → new_primEqInt(zu31100, zu3600)
new_esEs27(zu311010, zu36010, ty_@0) → new_esEs12(zu311010, zu36010)
new_esEs6(Just(zu311000), Just(zu36000), app(app(ty_Either, cc), cd)) → new_esEs19(zu311000, zu36000, cc, cd)
new_esEs19(Left(zu311000), Left(zu36000), ty_Integer, bbh) → new_esEs16(zu311000, zu36000)
new_esEs24(zu311000, zu36000, app(ty_Maybe, gc)) → new_esEs6(zu311000, zu36000, gc)
new_esEs13(@3(zu311000, zu311001, zu311002), @3(zu36000, zu36001, zu36002), fg, fh, ga) → new_asAs(new_esEs24(zu311000, zu36000, fg), new_asAs(new_esEs25(zu311001, zu36001, fh), new_esEs26(zu311002, zu36002, ga)))
new_esEs26(zu311002, zu36002, ty_@0) → new_esEs12(zu311002, zu36002)
new_esEs24(zu311000, zu36000, ty_Ordering) → new_esEs8(zu311000, zu36000)
new_esEs19(Right(zu311000), Right(zu36000), bdc, ty_Double) → new_esEs14(zu311000, zu36000)
new_esEs22(zu311000, zu36000, ty_Char) → new_esEs15(zu311000, zu36000)
new_esEs28(zu31100, zu3600, ty_Ordering) → new_esEs8(zu31100, zu3600)
new_esEs6(Just(zu311000), Just(zu36000), ty_Bool) → new_esEs7(zu311000, zu36000)
new_esEs8(LT, EQ) → False
new_esEs8(EQ, LT) → False
new_primEqInt(Pos(Succ(zu3110000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(zu360000))) → False
new_esEs19(Left(zu311000), Left(zu36000), ty_Bool, bbh) → new_esEs7(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_@0) → new_esEs12(zu311000, zu36000)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs19(Right(zu311000), Right(zu36000), bdc, ty_Integer) → new_esEs16(zu311000, zu36000)
new_esEs24(zu311000, zu36000, ty_Double) → new_esEs14(zu311000, zu36000)
new_deleteBy1([], :(:(zu3600, zu3601), zu361), ba) → :(:(zu3600, zu3601), new_deleteBy1([], zu361, ba))
The set Q consists of the following terms:
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_deleteBy1(x0, [], x1)
new_esEs27(x0, x1, ty_Integer)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primPlusNat1(Zero, Succ(x0))
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_@0)
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_deleteBy1(:(x0, x1), :(:(x2, x3), x4), x5)
new_esEs20(x0, x1, ty_Int)
new_esEs17(:(x0, x1), [], x2)
new_esEs26(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs22(x0, x1, ty_Bool)
new_esEs7(False, False)
new_esEs8(EQ, EQ)
new_sr(Pos(x0), Pos(x1))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Char)
new_esEs10(:%(x0, x1), :%(x2, x3), x4)
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs26(x0, x1, ty_Integer)
new_asAs(False, x0)
new_esEs26(x0, x1, ty_Bool)
new_esEs8(GT, GT)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Ordering)
new_esEs27(x0, x1, ty_Bool)
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs17([], [], x0)
new_esEs25(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Double)
new_esEs8(LT, LT)
new_esEs7(False, True)
new_esEs7(True, False)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs17([], :(x0, x1), x2)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs15(Char(x0), Char(x1))
new_deleteBy1([], :(:(x0, x1), x2), x3)
new_esEs22(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_esEs8(EQ, GT)
new_esEs8(GT, EQ)
new_esEs28(x0, x1, ty_Double)
new_deleteBy00(x0, x1, x2, x3, x4, True, x5)
new_deleteBy1([], :([], x0), x1)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Integer)
new_asAs(True, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs28(x0, x1, ty_Char)
new_esEs8(GT, LT)
new_esEs8(LT, GT)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs24(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Int)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_primMulNat0(Zero, Succ(x0))
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_deleteBy1(:(x0, x1), :([], x2), x3)
new_sr(Neg(x0), Neg(x1))
new_primEqNat0(Zero, Zero)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs25(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Int)
new_esEs25(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Integer)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_deleteBy00(x0, x1, x2, x3, x4, False, x5)
new_esEs12(@0, @0)
new_esEs6(Nothing, Just(x0), x1)
new_esEs27(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_primMulNat0(Zero, Zero)
new_esEs28(x0, x1, ty_Integer)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1)
new_esEs28(x0, x1, ty_Bool)
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_@0)
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Ordering)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Float)
new_esEs7(True, True)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs28(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs26(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Integer)
new_esEs16(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Int)
new_esEs28(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Char)
new_esEs28(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Double)
new_primEqNat0(Zero, Succ(x0))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Nothing, x1)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_@0)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs8(LT, EQ)
new_esEs8(EQ, LT)
new_esEs23(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs25(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Int)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs27(x0, x1, ty_@0)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs6(Just(x0), Just(x1), ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs23(x0, x1, ty_Float)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs28(x0, x1, ty_@0)
new_esEs28(x0, x1, ty_Float)
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs27(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Nothing, Nothing, x0)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldl(zu36, :(zu3110, zu3111), ba) → new_foldl(new_deleteBy1(zu3110, zu36, ba), zu3111, ba)
The graph contains the following edges 2 > 2, 3 >= 3
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_psPs(:(zu311111110, zu311111111), zu33, ba) → new_psPs(zu311111111, zu33, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs(:(zu311111110, zu311111111), zu33, ba) → new_psPs(zu311111111, zu33, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3